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

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

tests
0

failures
0

ignored
11m18.67s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.276s passed
powPositiveConcrete data()[101] 3.253s passed
powGeq1Concrete data()[102] 3.256s passed
pow2InIntLower data()[103] 3.252s passed
pow2InIntUpper data()[104] 3.284s passed
logSelfConcrete data()[105] 3.285s passed
log1Concrete data()[106] 3.272s passed
logProduct data()[107] 3.265s passed
logTimesBaseConcrete data()[108] 3.266s passed
logProdIdentity data()[109] 3.280s passed
moduloByteIsInByte data()[10] 3.363s passed
logProdIdentityConcrete data()[110] 3.292s passed
logPowIdentity data()[111] 3.298s passed
logPowIdentityConcrete data()[112] 3.266s passed
logPositive data()[113] 3.292s passed
logPositiveConcrete data()[114] 3.267s passed
logMono data()[115] 3.285s passed
logMonoConcrete data()[116] 3.259s passed
powLogLess data()[117] 3.271s passed
powLogMore2 data()[118] 3.282s passed
logLessThanPow data()[119] 3.300s passed
moduloCharIsInChar data()[11] 3.352s passed
logLessThanPowConcrete data()[120] 3.270s passed
logSqueeze data()[121] 3.268s passed
ifthenelse_equals data()[122] 3.275s passed
ifthenelse_equals_1 data()[123] 3.269s passed
ifthenelse_equals_2 data()[124] 3.272s passed
disjointWithSingleton1 data()[125] 3.257s passed
disjointWithSingleton2 data()[126] 3.254s passed
disjointArrayRanges data()[127] 3.256s passed
disjointArrayRangeAllFields1 data()[128] 3.271s passed
disjointArrayRangeAllFields2 data()[129] 3.272s passed
div_unique1 data()[12] 3.422s passed
seqSelfDefinition data()[130] 3.269s passed
seqOutsideValue data()[131] 3.262s passed
castedGetAny data()[132] 3.266s passed
seqGetAlphaCast data()[133] 3.262s passed
getOfSeqSingleton data()[134] 3.279s passed
getOfSeqSingletonConcrete data()[135] 3.254s passed
getOfSeqConcat data()[136] 3.267s passed
getOfSeqSub data()[137] 3.313s passed
getOfSeqReverse data()[138] 3.319s passed
lenOfSeqEmpty data()[139] 3.272s passed
div_unique2 data()[13] 3.430s passed
lenOfSeqSingleton data()[140] 3.319s passed
lenOfSeqConcat data()[141] 3.285s passed
lenOfSeqSub data()[142] 3.274s passed
lenOfSeqReverse data()[143] 3.261s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.266s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.310s passed
getOfSeqSingletonEQ data()[146] 3.286s passed
getOfSeqConcatEQ data()[147] 3.289s passed
getOfSeqSubEQ data()[148] 3.266s passed
getOfSeqReverseEQ data()[149] 3.277s passed
div_exists data()[14] 3.611s passed
lenOfSeqEmptyEQ data()[150] 3.296s passed
lenOfSeqSingletonEQ data()[151] 3.283s passed
lenOfSeqConcatEQ data()[152] 3.277s passed
lenOfSeqSubEQ data()[153] 3.274s passed
lenOfSeqReverseEQ data()[154] 3.299s passed
getOfSeqDefEQ data()[155] 3.274s passed
lenOfSeqDefEQ data()[156] 3.274s passed
seqConcatWithSeqEmpty1 data()[157] 3.299s passed
seqConcatWithSeqEmpty2 data()[158] 3.309s passed
seqReverseOfSeqEmpty data()[159] 3.282s passed
div_one data()[15] 3.350s passed
subSeqComplete data()[160] 3.291s passed
subSeqTailR data()[161] 3.327s passed
subSeqTailL data()[162] 3.301s passed
subSeqTailEQR data()[163] 3.310s passed
subSeqTailEQL data()[164] 3.327s passed
seqDef_split data()[165] 3.326s passed
seqDef_induction_upper data()[166] 3.368s passed
seqDef_induction_upper_concrete data()[167] 3.336s passed
seqDef_induction_lower data()[168] 3.333s passed
seqDef_induction_lower_concrete data()[169] 3.348s passed
jdiv_one data()[16] 3.362s passed
seqDef_split_in_three data()[170] 3.428s passed
seqDef_empty data()[171] 3.347s passed
seqDef_one_summand data()[172] 3.323s passed
seqDef_lower_equals_upper data()[173] 3.309s passed
seqDefOfSeq data()[174] 3.308s passed
seqSelfDefinitionEQ2 data()[175] 3.341s passed
indexOfSeqSingleton data()[176] 3.305s passed
indexOfSeqConcatFirst data()[177] 3.341s passed
indexOfSeqConcatSecond data()[178] 3.328s passed
indexOfSeqSub data()[179] 3.341s passed
div_zero data()[17] 3.381s passed
lenOfArray2seq data()[180] 3.291s passed
getAnyOfArray2seq data()[181] 3.338s passed
getOfArray2seq data()[182] 3.307s passed
getAnyOfNPermInv data()[183] 3.331s passed
seqNPermRange data()[184] 3.363s passed
seqPermTrans data()[185] 3.334s passed
seqPermRefl data()[186] 3.366s passed
seqPermSplit data()[187] 3.327s passed
seqNPermRight data()[188] 3.521s passed
seqPermFromSwap data()[189] 3.388s passed
divResZero1 data()[18] 3.365s passed
seqPermTransAlt0 data()[190] 3.304s passed
seqPermTransAlt1 data()[191] 3.318s passed
seqPermTransAlt2 data()[192] 3.320s passed
seqPermTransAlt3 data()[193] 3.339s passed
seqPermForall data()[194] 3.477s passed
seqPermExists data()[195] 3.426s passed
schiffl_lemma_2 data()[196] 23.065s passed
schiffl_thm_1 data()[197] 4.106s passed
eqSameSeq data()[198] 3.385s passed
divResZero2 data()[19] 3.368s passed
eqTermCut data()[1] 4.033s passed
divResOne1 data()[20] 3.371s passed
divResOne2 data()[21] 3.347s passed
div_cancel1 data()[22] 3.366s passed
div_cancel2 data()[23] 3.331s passed
divAddMultDenom data()[24] 3.346s passed
divMinus data()[25] 3.406s passed
divMinusDenom data()[26] 3.367s passed
divLeastDPos data()[27] 3.319s passed
divLeastDNeg data()[28] 3.318s passed
divGreatestDPos data()[29] 3.349s passed
equivAllRight data()[2] 3.758s passed
divGreatestDNeg data()[30] 3.339s passed
divIncreasingPos data()[31] 3.328s passed
divIncreasingNeg data()[32] 3.321s passed
jdiv_zero data()[33] 3.311s passed
jdivPulloutMinusNum data()[34] 3.315s passed
jdivPulloutMinusDenom data()[35] 3.347s passed
jdiv_uniquePosPos data()[36] 3.344s passed
jdiv_uniquePosNeg data()[37] 3.351s passed
jdiv_uniqueNegPos data()[38] 3.358s passed
jdiv_uniqueNegNeg data()[39] 3.332s passed
irrflConcrete1 data()[3] 3.773s passed
jdivMultDenom1 data()[40] 3.352s passed
jdivMultDenom2 data()[41] 3.312s passed
mod_geZero data()[42] 3.292s passed
mod_lessDenom data()[43] 3.324s passed
jmod_NumPos data()[44] 3.299s passed
jmod_NumNeg data()[45] 3.318s passed
jmod_geZero data()[46] 3.299s passed
jmodNumZero data()[47] 3.303s passed
jmod_pulloutminusNum data()[48] 3.304s passed
jmod_pulloutminusDenom data()[49] 3.291s passed
irrflConcrete2 data()[4] 3.545s passed
jmodUnique1 data()[50] 3.358s passed
jmodUnique2 data()[51] 3.359s passed
intDivRem data()[52] 3.289s passed
jmodjmod data()[53] 3.428s passed
jmodDivisible data()[54] 3.340s passed
jmodDivisibleRep data()[55] 3.304s passed
jdivAddMultDenom data()[56] 3.475s passed
jmodAltZero data()[57] 3.310s passed
jmodAddMultDenomZero data()[58] 3.311s passed
polyDiv_zero data()[59] 3.315s passed
cancel_gtPos data()[5] 3.480s passed
polyMod_ltdivDenom data()[60] 3.292s passed
bsum_empty data()[61] 3.282s passed
bsum_induction_upper data()[62] 3.277s passed
bsum_induction_lower data()[63] 3.315s passed
bsum_num_of_bounds data()[64] 3.325s passed
bsum_num_of_bounds2 data()[65] 3.321s passed
bsum_induction_upper2 data()[66] 3.278s passed
bsum_induction_upper_concrete data()[67] 3.296s passed
bsum_induction_upper_concrete_2 data()[68] 3.274s passed
bsum_induction_upper2_concrete data()[69] 3.277s passed
cancel_gtNeg data()[6] 3.456s passed
bsum_induction_lower_concrete data()[70] 3.280s passed
bsum_induction_lower2 data()[71] 3.287s passed
bsum_induction_lower2_concrete data()[72] 3.275s passed
bsum_positive data()[73] 3.338s passed
bsum_upper_bound data()[74] 3.356s passed
bsum_lower_bound data()[75] 3.293s passed
bsum_positive_lower_bound_element data()[76] 3.331s passed
bsum_sub_same_index data()[77] 3.326s passed
bsum_less_same_index data()[78] 3.306s passed
bsum_equal_except_one_index data()[79] 3.302s passed
moduloIntIsInInt data()[7] 3.408s passed
bsum_num_of_is_max data()[80] 3.334s passed
bsum_num_of_is_max2 data()[81] 3.298s passed
bsum_num_of_is_max3 data()[82] 3.300s passed
bsum_num_of_is_max4 data()[83] 3.289s passed
bsum_num_of_lt_max data()[84] 3.273s passed
bsum_num_of_lt_max2 data()[85] 3.287s passed
bsum_num_of_lt_max3 data()[86] 3.277s passed
bsum_num_of_lt_max4 data()[87] 3.270s passed
bsum_num_of_gt0 data()[88] 3.268s passed
bsum_num_of_gt0_alt data()[89] 3.266s passed
moduloLongIsInLong data()[8] 3.395s passed
bsum_add_concrete data()[90] 3.274s passed
bprod_all_positive data()[91] 3.263s passed
bprod_split data()[92] 3.285s passed
powConcrete0 data()[93] 3.255s passed
powConcrete1 data()[94] 3.246s passed
powSplitFactor data()[95] 3.245s passed
powAdd data()[96] 3.243s passed
powMono data()[97] 3.246s passed
powMonoConcrete data()[98] 3.249s passed
powMonoConcreteRight data()[99] 3.242s passed
moduloShortIsInShort data()[9] 3.359s passed

Standard output

612        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
639        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.82ms 
844        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
860        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)

1763       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1765       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1766       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1766       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3330       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9269       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.42s 
9335       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9371       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ns 
9384       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9386       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.97ms 
9391       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
12402      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13408      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.51ms 
13419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.8ns 
13421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
16268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17175      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms 
17177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns 
17182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
20061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20943      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
20952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 484.1ns 
20954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
23653      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
24488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24494      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
24497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24497      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 
24499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
27110      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.98ms 
27978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 575.8ns 
27982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
30576      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.82ms 
31435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.8ns 
31437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
34029      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34841      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885.1ns 
34843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34843      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
34844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
37424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
38236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.3ns 
38238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
38239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.6ns 
38240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
40787      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41595      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.4ns 
41597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.1ns 
41599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
44152      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44958      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.3ns 
44960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134ns 
44961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
47504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48309      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.5ns 
48313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.9ns 
48322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
50888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51732      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.64ms 
51737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51738      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.1ns 
51739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
54284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55164      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.19ms 
55167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55167      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.7ns 
55168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
57710      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 248.08ms 
58778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.2ns 
58779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
61301      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
62127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
62128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
64659      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65487      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
65491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.2ns 
65493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
68006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
68870      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.53ms 
68872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
68872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
68873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
71386      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
72238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.9ns 
72239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74751      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
74752      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75603      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
75607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.2ns 
75614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
78136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
78957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
78974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
78977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
78977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367ns 
78978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
81486      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82320      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms 
82323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.8ns 
82326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84842      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
84842      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
85686      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.4ms 
85689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.9ns 
85691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
88198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89018      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
89019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89020      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
89021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
91507      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
92321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
92364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.65ms 
92366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
92366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
92367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
94890      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
95712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
95770      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.64ms 
95772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
95773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.3ns 
95774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98276      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
98276      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99137      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.54ms 
99139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 
99140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
101627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
102448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
102456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
102458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
102458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
102459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
104945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
105759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
105774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.94ms 
105776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
105777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.1ns 
105778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
108296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
109112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
109123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
109125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
109125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
109126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
111635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
112454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
112463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
112464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
112464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns 
112465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
114955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
115782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
115790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
115793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
115793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.6ns 
115794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
118287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
119103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
119110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
119113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
119114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.5ns 
119115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
121595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
122418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
122422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
122424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
122424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
122425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
124904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
125721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
125737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.51ms 
125739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
125739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
125741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
128221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
129034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
129084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.79ms 
129086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
129086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
129087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
131586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
132404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
132426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
132430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
132430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
132431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
134937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
135760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
135779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ms 
135780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
135780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
135781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
138291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
139115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
139136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
139139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
139140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 
139141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
141631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
142452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
142469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
142472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
142472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.42ns 
142473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
144954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
145781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
145821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.89ms 
145824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
145824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.6ns 
145825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
148314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
149127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
149133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
149138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
149139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
149141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
151614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
152424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
152429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
152430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
152430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.91ns 
152431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
154924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
155741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
155749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
155754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
155754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
155755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
158229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
159042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
159051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
159053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
159054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.12ns 
159055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
161542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
162351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
162369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
162370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
162371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
162371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
164851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
165660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
165668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
165670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
165670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
165671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
168147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
168966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
168970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
168974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
168974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.71ns 
168975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
171464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
172272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
172275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
172277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
172277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
172278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
174753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
175562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
175566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
175568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
175568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
175569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
178037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
178846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
178924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.9ms 
178927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
178927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.31ns 
178928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
181398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
182208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
182283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.98ms 
182285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
182285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
182286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
184759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
185568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
185572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
185573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
185573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
185574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
188144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
188965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
189000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.77ms 
189001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
189002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.81ns 
189002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
191483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
192312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
192340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.35ms 
192342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
192342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
192343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
194824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
195639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
195643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
195648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
195649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.31ns 
195650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
198150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
198962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
199120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.26ms 
199122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
199122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.1ns 
199123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
201610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
202420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
202431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
202433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
202433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
202433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
204922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
205734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
205742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
205744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
205744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
205745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
208230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
209041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
209057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
209059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
209059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
209060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
211531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
212336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
212349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
212351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
212351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
212352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
214827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
215627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
215631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
215632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
215632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
215633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
218094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
218904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
218908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
218910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
218910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
218911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
221386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
222193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
222221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 
222226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
222226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.7ns 
222228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
224722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
225532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
225549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
225550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
225550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
225551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
228041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
228851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
228870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.72ms 
228872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
228873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.41ns 
228874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
231338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
232144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
232148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
232150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
232151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.5ns 
232151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
234635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
235440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
235445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
235446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
235446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
235447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
237909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
238712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
238718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
238719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
238719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
238720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
241179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
241992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
241995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
241997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
241997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
241998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
244466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
245273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
245275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.72ns 
245277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
245277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
245278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
247750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
248559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
248563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
248564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
248564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
248565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
251028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
251835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
251838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.83ns 
251839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
251839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
251840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
254306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
255113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
255174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.19ms 
255177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
255177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 
255179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
257686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
258487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
258531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.72ms 
258533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
258533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
258534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
260985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
261785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
261825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.6ms 
261826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
261826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
261827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
264316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
265101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
265154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.63ms 
265157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
265157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.5ns 
265158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
267665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
268450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
268481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.04ms 
268483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
268483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
268484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
270961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
271739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
271788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.86ms 
271789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
271790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
271790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
274282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
275063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
275089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.25ms 
275091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
275091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
275092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
277620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
278404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
278423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.63ms 
278425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
278425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
278426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
280918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
281697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
281721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.37ms 
281722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
281722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
281723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
284215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
284999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
285021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.41ms 
285023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
285024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.31ns 
285025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
287505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
288284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
288310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
288312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
288312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
288313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
290781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
291560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
291583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.95ms 
291584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
291585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
291585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
294067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
294847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
294870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
294871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
294872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
294872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
297337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
298115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
298147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.38ms 
298149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
298149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.4ns 
298150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
300620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
301397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
301417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.07ms 
301418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
301418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
301419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
303885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
304661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
304686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.3ms 
304687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
304687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
304688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
307147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
307923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
307951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.32ms 
307953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
307954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
307955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
310437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
311218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
311226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
311228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
311228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
311229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
313692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
314473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
314490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
314491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
314491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
314492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
316984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
317770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
317774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
317777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
317777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.3ns 
317778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
320249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
321027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
321029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.61ns 
321031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
321031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
321031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
323492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
324273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
324275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.91ns 
324276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
324277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
324277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
326736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
327514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
327521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
327522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
327522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
327523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
329981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
330757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
330764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
330765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
330765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
330766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
333220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
333997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
334009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
334010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
334010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
334011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
336477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
337255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
337258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
337260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
337260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
337260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
339720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
340498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
340501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.71ns 
340502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
340502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
340503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
342977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
343770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
343776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
343777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
343777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
343778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
346247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
347027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
347030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.41ns 
347031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
347031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
347032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
349504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
350284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
350286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.4ns 
350287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
350287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
350288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
352754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
353535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
353537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.4ns 
353539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
353539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
353539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
356028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
356818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
356822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
356823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
356823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
356824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
359315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
360097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
360106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms 
360108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
360108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
360109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
362589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
363374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
363378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
363379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
363379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
363380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
365854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
366636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
366643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
366645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
366645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
366645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
369125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
369905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
369910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
369911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
369911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
369912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
372384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
373166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
373189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
373190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
373190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
373191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
375692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
376477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
376481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
376482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
376483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
376483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
378965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
379776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
379780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
379781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
379781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
379782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
382232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
383041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
383045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
383046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
383046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
383047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
385509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
386320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
386337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
386339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
386339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
386340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
388796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
389599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
389604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.11ns 
389606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
389606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
389607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
392051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
392852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
392889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.79ms 
392891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
392891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
392891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
395339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
396145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
396149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
396150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
396150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
396151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
398596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
399398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
399419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
399420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
399420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
399421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
401877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
402681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
402702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.42ms 
402703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
402703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
402704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
405169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
405978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
406001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.25ms 
406003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
406003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
406003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
408460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
409269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
409271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.81ns 
409274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
409274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.1ns 
409275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
411728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
412533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
412539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
412540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
412541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
412541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
415003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
415811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
415815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
415816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
415816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
415817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
418275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
419081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
419084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920.31ns 
419085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
419085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
419086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
421545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
422353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
422355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 926.3ns 
422357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
422357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116ns 
422357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
424796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
425608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
425612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
425617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
425617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
425618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
428058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
428866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
428868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
428870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
428870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
428871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
431306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
432115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
432124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
432125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
432125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
432126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
434577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
435384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
435395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
435396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
435396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
435397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
437849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
438657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
438667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
438669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
438669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
438670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
441110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
441923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
441936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
441937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
441937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
441938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
444374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
445194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
445198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
445200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
445200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
445201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
447643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
448458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
448464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
448466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
448466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
448466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
450906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
451724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
451726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.01ns 
451728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
451728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
451728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
454175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
455002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
455005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
455006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
455006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
455007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
457442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
458257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
458260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.21ns 
458261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
458261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
458262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
460722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
461515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
461526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
461527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
461527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
461528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
464033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
464829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
464838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
464841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
464841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns 
464843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
467323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
468118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
468159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
468160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
468160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
468161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
470609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
471428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
471431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 768.81ns 
471432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
471432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
471433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
473923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
474747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
474750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.11ns 
474751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
474751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
474752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
477210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
478031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
478035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
478036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
478036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
478037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
480485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
481305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
481308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
481309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
481309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
481310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
483749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
484566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
484569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
484570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
484570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
484571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
487037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
487832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
487835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
487837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
487837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
487838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
490321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
491140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
491145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
491146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
491146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
491147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
493610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
494429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
494432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
494433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
494433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
494434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
496890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
497709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
497720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
497721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
497722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
497722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
500167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
500984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
500986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.81ns 
500987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
500987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
500988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
503461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
504257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
504264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
504265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
504265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
504266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
506737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
507556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
507559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.11ns 
507562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
507562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.1ns 
507563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
510022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
510841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
510843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.41ns 
510845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
510845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
510845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
513293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
514113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
514118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
514123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
514123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.9ns 
514124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
516598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
517391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
517394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
517395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
517396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
517396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
519870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
520688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
520693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
520694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
520695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
520695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
523145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
523964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
523967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
523969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
523969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
523969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
526418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
527237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
527241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
527243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
527243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
527244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
529730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
530525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
530540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
530541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
530541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
530542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
533016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
533835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
533849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
533851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
533851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
533852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
536302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
537122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
537132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
537133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
537133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
537134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
539616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
540412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
540423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
540424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
540424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
540425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
542906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
543725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
543749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.71ms 
543750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
543751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
543751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
546206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
547026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
547050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.87ms 
547051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
547051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
547052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
549532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
550336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
550360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms 
550361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
550361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
550362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
552851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
553672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
553687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
553689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
553689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
553690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
556157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
556978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
557013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.13ms 
557015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
557015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
557016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
559504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
560304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
560381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.42ms 
560383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
560383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
560383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
562859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
563681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
563718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.42ms 
563719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
563719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
563720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
566211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
567010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
567050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.61ms 
567052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
567052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
567052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
569539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
570357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
570399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.75ms 
570400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
570400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
570401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
572880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
573710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
573825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.93ms 
573827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
573827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
573828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
576337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
577165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
577173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
577175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
577175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
577176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
579665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
580488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
580496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
580497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
580497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
580498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
582983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
583800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
583806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
583807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
583807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
583808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
586271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
587095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
587113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
587115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
587115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
587115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
589619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
590443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
590454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
590456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
590456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
590457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
592932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
593755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
593759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
593760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
593760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
593761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
596258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
597084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
597101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
597102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
597102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
597103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
599586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
600412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
600428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
600429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
600429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
600430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
602928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
603751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
603770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.06ms 
603771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
603771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
603772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
606234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
607057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
607060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
607062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
607062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
607062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
609571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
610394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
610398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
610399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
610400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
610400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
612877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
613699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
613706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
613707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
613707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
613708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
616205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
617029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
617036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
617037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
617037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
617038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
619509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
620330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
620399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.78ms 
620400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
620400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
620401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
622884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
623706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
623733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.92ms 
623735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
623735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
623735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
626254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
627077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
627099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.14ms 
627100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
627100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
627101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
629601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
630424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
630427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.6ns 
630428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
630428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
630429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
632929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
633753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
633947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182.65ms 
633950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
633950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
633951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
636458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
637284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
637335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.39ms 
637336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
637337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
637337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
639815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
640637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
640639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.5ns 
640641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
640641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
640641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
643130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
643955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
643957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 388.7ns 
643959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
643959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
643959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
646441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
647275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
647277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.1ns 
647280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
647280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
647281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
649783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
650614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
650616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.5ns 
650617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
650617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
650618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
653138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
653969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
654093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 121.03ms 
654095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
654095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274ns 
654096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
656640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
657469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
657519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.82ms 
657521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
657521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
657522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
660046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
660882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
660883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 
660911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
660954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
660972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
660976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
660983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
660987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
660988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
660990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
660994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
660996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
660999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
661000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
661197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
661198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
661199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
661201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
661202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
661311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
661313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
661314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
661316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
661317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
661318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
661469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
661471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
661472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
661473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
661474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
661481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
661631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
661633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
661635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
661636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
661636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
661637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
661646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
661647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
661648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
661650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
661652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
661653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
661665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
661666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
661667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
661668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
661669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
661670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
661838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
661839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
661840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
661954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
661955     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)'' 
661958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
661959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
661960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
661961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
661962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
661962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
661966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
661967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
661968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
661969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
661970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
662073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
662077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
662079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
662080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
662081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
662082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
662083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
662195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
662197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
662198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
662200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
662200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
662201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
662202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
662204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
662290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
662292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
662418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
662422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
662426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
662427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
662428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
662430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
662430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
662431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
662432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
662433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
662440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
662445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
662538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
662540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
662541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
662542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
662543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
662543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
662544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
662545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
662598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
662604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
662702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
662703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
662705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
662707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
662707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
662708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
662843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
662847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
662849     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)'' 
662851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
662852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
662853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
662854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
662854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
662863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
662865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
662866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
662867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
662972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
662973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
662974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
662975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
662976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
662977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
663082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
663083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
663085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
663086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
663087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
663088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
663089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
663090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
663174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
663176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
663255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
663256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
663257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
663262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
663267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
663271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
663398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
663399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
663400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
663406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
663417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
663513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
667504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
667505     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)'' 
667511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
667512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
667513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
667515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
667516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
667524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
667526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
667527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
667528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
667529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
667623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
667627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
667629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
667630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
667630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
667631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
667632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
667728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
667729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
667730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
667732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
667732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
667733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
667734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
667735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
667811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
667812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
667886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
667890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
667895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
667896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
667897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
667898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
667908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
667990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
667991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
667992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
667993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
668067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
668077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
668078     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)'' 
668080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
668081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
668082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
668083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
668083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
668094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
668096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
668097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
668098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
668098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
668186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
668187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
668189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
668189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
668190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
668287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
668292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
668294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
668294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
668295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
668295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
668296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
668395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
668397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
668398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
668399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
668401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
668403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
668404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
668407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
668409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
668409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
668410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
668411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
668411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
668411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
668412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
668503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
668505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
668511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
668590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
668672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
668673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
668674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
668675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
668676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
668676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
668677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
668677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
668679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
668766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
668775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
668866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
668868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
668869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
668870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
668871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
668871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
668871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
668872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
668878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
668879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
668959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
668964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
668970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
669070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
669071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
669072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
669073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
669073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
669073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
669074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
669074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
669129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
669131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
669131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
669132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
669133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
669139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
669144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
669307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
669394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
669396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
669396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
669397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
669562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
669649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
669650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
672756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
672761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
672762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
672762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
672763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
672877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
672878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
672879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
672880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
672880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
672985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
676073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
679353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
679357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
679358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
679359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
679360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
679472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
679473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
679474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
679475     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)' ...' 
679477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
680586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
680586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
680587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
683142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
683985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
683987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
683987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
683994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
684004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
684006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
684008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
684008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
684013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
684014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
684016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
684019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
684019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
684028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
684029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
684030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
684076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
684077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
684078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
684078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
684079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
684142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
684143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
684144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
684145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
684145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
684149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
684149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
684149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
684150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
684151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
684151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
684234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
684235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
684235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
684236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
684237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
684238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
684328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
684329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
684330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
684330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
684331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
684332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
684332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
684332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
684333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
684333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
684334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
684334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
684334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
684335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
684335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
684336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
684336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
684337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
684338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
684340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
684378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
684379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
684436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
684437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
684438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
684439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
684440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
684440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
684493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
684496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
684497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
684499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
684500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
684500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
684501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
684558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
684560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
684563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
684629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
684692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
684692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
684693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
687192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
688042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
688074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.33ms