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

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

tests
0

failures
0

ignored
14m9.14s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.026s passed
powPositiveConcrete data()[101] 4.035s passed
powGeq1Concrete data()[102] 4.111s passed
pow2InIntLower data()[103] 4.015s passed
pow2InIntUpper data()[104] 4.056s passed
logSelfConcrete data()[105] 4.053s passed
log1Concrete data()[106] 4.142s passed
logProduct data()[107] 4.036s passed
logTimesBaseConcrete data()[108] 4.096s passed
logProdIdentity data()[109] 4.038s passed
moduloByteIsInByte data()[10] 4.195s passed
logProdIdentityConcrete data()[110] 4.132s passed
logPowIdentity data()[111] 3.998s passed
logPowIdentityConcrete data()[112] 4.052s passed
logPositive data()[113] 4.010s passed
logPositiveConcrete data()[114] 4.077s passed
logMono data()[115] 4.086s passed
logMonoConcrete data()[116] 4.108s passed
powLogLess data()[117] 4.125s passed
powLogMore2 data()[118] 4.053s passed
logLessThanPow data()[119] 4.127s passed
moduloCharIsInChar data()[11] 4.180s passed
logLessThanPowConcrete data()[120] 4.073s passed
logSqueeze data()[121] 4.105s passed
ifthenelse_equals data()[122] 4.171s passed
ifthenelse_equals_1 data()[123] 4.097s passed
ifthenelse_equals_2 data()[124] 4.127s passed
disjointWithSingleton1 data()[125] 4.072s passed
disjointWithSingleton2 data()[126] 4.069s passed
disjointArrayRanges data()[127] 4.058s passed
disjointArrayRangeAllFields1 data()[128] 4.081s passed
disjointArrayRangeAllFields2 data()[129] 4.076s passed
div_unique1 data()[12] 4.357s passed
seqSelfDefinition data()[130] 4.115s passed
seqOutsideValue data()[131] 4.114s passed
castedGetAny data()[132] 4.134s passed
seqGetAlphaCast data()[133] 4.084s passed
getOfSeqSingleton data()[134] 4.092s passed
getOfSeqSingletonConcrete data()[135] 4.070s passed
getOfSeqConcat data()[136] 4.082s passed
getOfSeqSub data()[137] 4.181s passed
getOfSeqReverse data()[138] 4.065s passed
lenOfSeqEmpty data()[139] 4.129s passed
div_unique2 data()[13] 4.223s passed
lenOfSeqSingleton data()[140] 4.093s passed
lenOfSeqConcat data()[141] 4.112s passed
lenOfSeqSub data()[142] 4.131s passed
lenOfSeqReverse data()[143] 4.080s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.092s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.118s passed
getOfSeqSingletonEQ data()[146] 4.038s passed
getOfSeqConcatEQ data()[147] 4.132s passed
getOfSeqSubEQ data()[148] 4.119s passed
getOfSeqReverseEQ data()[149] 4.142s passed
div_exists data()[14] 4.393s passed
lenOfSeqEmptyEQ data()[150] 4.178s passed
lenOfSeqSingletonEQ data()[151] 4.191s passed
lenOfSeqConcatEQ data()[152] 4.268s passed
lenOfSeqSubEQ data()[153] 4.103s passed
lenOfSeqReverseEQ data()[154] 4.085s passed
getOfSeqDefEQ data()[155] 4.113s passed
lenOfSeqDefEQ data()[156] 4.102s passed
seqConcatWithSeqEmpty1 data()[157] 4.156s passed
seqConcatWithSeqEmpty2 data()[158] 4.232s passed
seqReverseOfSeqEmpty data()[159] 4.128s passed
div_one data()[15] 4.146s passed
subSeqComplete data()[160] 4.173s passed
subSeqTailR data()[161] 4.166s passed
subSeqTailL data()[162] 4.279s passed
subSeqTailEQR data()[163] 4.281s passed
subSeqTailEQL data()[164] 4.224s passed
seqDef_split data()[165] 4.175s passed
seqDef_induction_upper data()[166] 4.236s passed
seqDef_induction_upper_concrete data()[167] 4.161s passed
seqDef_induction_lower data()[168] 4.144s passed
seqDef_induction_lower_concrete data()[169] 4.188s passed
jdiv_one data()[16] 4.124s passed
seqDef_split_in_three data()[170] 4.276s passed
seqDef_empty data()[171] 4.137s passed
seqDef_one_summand data()[172] 4.086s passed
seqDef_lower_equals_upper data()[173] 4.091s passed
seqDefOfSeq data()[174] 4.097s passed
seqSelfDefinitionEQ2 data()[175] 4.054s passed
indexOfSeqSingleton data()[176] 4.119s passed
indexOfSeqConcatFirst data()[177] 4.175s passed
indexOfSeqConcatSecond data()[178] 4.130s passed
indexOfSeqSub data()[179] 4.121s passed
div_zero data()[17] 4.156s passed
lenOfArray2seq data()[180] 4.108s passed
getAnyOfArray2seq data()[181] 4.171s passed
getOfArray2seq data()[182] 4.125s passed
getAnyOfNPermInv data()[183] 4.163s passed
seqNPermRange data()[184] 4.251s passed
seqPermTrans data()[185] 4.211s passed
seqPermRefl data()[186] 4.118s passed
seqPermSplit data()[187] 4.073s passed
seqNPermRight data()[188] 4.419s passed
seqPermFromSwap data()[189] 4.259s passed
divResZero1 data()[18] 4.075s passed
seqPermTransAlt0 data()[190] 4.172s passed
seqPermTransAlt1 data()[191] 4.179s passed
seqPermTransAlt2 data()[192] 4.081s passed
seqPermTransAlt3 data()[193] 4.129s passed
seqPermForall data()[194] 4.245s passed
seqPermExists data()[195] 4.215s passed
schiffl_lemma_2 data()[196] 27.826s passed
schiffl_thm_1 data()[197] 5.171s passed
eqSameSeq data()[198] 4.323s passed
divResZero2 data()[19] 4.059s passed
eqTermCut data()[1] 4.982s passed
divResOne1 data()[20] 4.130s passed
divResOne2 data()[21] 4.186s passed
div_cancel1 data()[22] 4.131s passed
div_cancel2 data()[23] 4.066s passed
divAddMultDenom data()[24] 4.186s passed
divMinus data()[25] 4.219s passed
divMinusDenom data()[26] 4.202s passed
divLeastDPos data()[27] 4.162s passed
divLeastDNeg data()[28] 4.142s passed
divGreatestDPos data()[29] 4.140s passed
equivAllRight data()[2] 4.642s passed
divGreatestDNeg data()[30] 4.116s passed
divIncreasingPos data()[31] 4.176s passed
divIncreasingNeg data()[32] 4.087s passed
jdiv_zero data()[33] 4.060s passed
jdivPulloutMinusNum data()[34] 4.017s passed
jdivPulloutMinusDenom data()[35] 4.165s passed
jdiv_uniquePosPos data()[36] 4.121s passed
jdiv_uniquePosNeg data()[37] 4.052s passed
jdiv_uniqueNegPos data()[38] 4.079s passed
jdiv_uniqueNegNeg data()[39] 4.218s passed
irrflConcrete1 data()[3] 4.634s passed
jdivMultDenom1 data()[40] 4.091s passed
jdivMultDenom2 data()[41] 4.129s passed
mod_geZero data()[42] 4.196s passed
mod_lessDenom data()[43] 4.168s passed
jmod_NumPos data()[44] 4.263s passed
jmod_NumNeg data()[45] 4.248s passed
jmod_geZero data()[46] 4.193s passed
jmodNumZero data()[47] 4.112s passed
jmod_pulloutminusNum data()[48] 4.153s passed
jmod_pulloutminusDenom data()[49] 4.082s passed
irrflConcrete2 data()[4] 4.497s passed
jmodUnique1 data()[50] 4.216s passed
jmodUnique2 data()[51] 4.513s passed
intDivRem data()[52] 4.351s passed
jmodjmod data()[53] 4.291s passed
jmodDivisible data()[54] 4.352s passed
jmodDivisibleRep data()[55] 4.363s passed
jdivAddMultDenom data()[56] 4.348s passed
jmodAltZero data()[57] 4.256s passed
jmodAddMultDenomZero data()[58] 4.212s passed
polyDiv_zero data()[59] 4.212s passed
cancel_gtPos data()[5] 4.420s passed
polyMod_ltdivDenom data()[60] 4.132s passed
bsum_empty data()[61] 4.098s passed
bsum_induction_upper data()[62] 4.072s passed
bsum_induction_lower data()[63] 4.104s passed
bsum_num_of_bounds data()[64] 4.108s passed
bsum_num_of_bounds2 data()[65] 4.115s passed
bsum_induction_upper2 data()[66] 4.118s passed
bsum_induction_upper_concrete data()[67] 4.106s passed
bsum_induction_upper_concrete_2 data()[68] 4.159s passed
bsum_induction_upper2_concrete data()[69] 4.140s passed
cancel_gtNeg data()[6] 4.376s passed
bsum_induction_lower_concrete data()[70] 4.119s passed
bsum_induction_lower2 data()[71] 4.168s passed
bsum_induction_lower2_concrete data()[72] 4.127s passed
bsum_positive data()[73] 4.297s passed
bsum_upper_bound data()[74] 4.234s passed
bsum_lower_bound data()[75] 4.212s passed
bsum_positive_lower_bound_element data()[76] 4.310s passed
bsum_sub_same_index data()[77] 4.261s passed
bsum_less_same_index data()[78] 4.301s passed
bsum_equal_except_one_index data()[79] 4.242s passed
moduloIntIsInInt data()[7] 4.371s passed
bsum_num_of_is_max data()[80] 4.167s passed
bsum_num_of_is_max2 data()[81] 4.208s passed
bsum_num_of_is_max3 data()[82] 4.179s passed
bsum_num_of_is_max4 data()[83] 4.097s passed
bsum_num_of_lt_max data()[84] 4.097s passed
bsum_num_of_lt_max2 data()[85] 4.138s passed
bsum_num_of_lt_max3 data()[86] 4.198s passed
bsum_num_of_lt_max4 data()[87] 4.125s passed
bsum_num_of_gt0 data()[88] 4.143s passed
bsum_num_of_gt0_alt data()[89] 4.094s passed
moduloLongIsInLong data()[8] 4.275s passed
bsum_add_concrete data()[90] 4.089s passed
bprod_all_positive data()[91] 4.138s passed
bprod_split data()[92] 4.097s passed
powConcrete0 data()[93] 4.132s passed
powConcrete1 data()[94] 4.195s passed
powSplitFactor data()[95] 4.067s passed
powAdd data()[96] 4.071s passed
powMono data()[97] 4.097s passed
powMonoConcrete data()[98] 4.076s passed
powMonoConcreteRight data()[99] 4.025s passed
moduloShortIsInShort data()[9] 4.235s passed

Standard output

489        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
516        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10ms 
829        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862        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)

2097       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2099       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2103       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2104       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3636       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.55s 
10466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10516      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.8ns 
10535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.3ns 
10540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
14259      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.69ms 
15528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 
15530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
19007      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20167      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
20170      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.1ns 
20172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23732      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
23733      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24800      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
24807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.2ns 
24808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28219      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
28221      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
29304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.6ns 
29306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
32541      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33719      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.14ms 
33731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.55ms 
33735      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
36954      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38099      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.98ms 
38106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 498.4ns 
38112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
41447      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.2ns 
42477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.5ns 
42479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
45666      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46748      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.5ns 
46751      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.1ns 
46753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
49930      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50984      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.1ns 
50987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.4ns 
50989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
54131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55180      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.2ns 
55183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55184      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.2ns 
55185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
58367      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
59360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.2ns 
59363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
59364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.1ns 
59365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
62575      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.52ms 
63719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
63721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
66829      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67940      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.1ms 
67944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67945      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.3ns 
67948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
71093      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
72147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
72334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.62ms 
72338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
72339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.2ns 
72340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
75487      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
76475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
76482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
76484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
76484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
76485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
79595      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
80602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
80606      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
80615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
80616      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 871.4ns 
80619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
83722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
84769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.36ms 
84772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
84772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.8ns 
84773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
87814      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
88821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
88844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.28ms 
88846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
88846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309ns 
88848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
91906      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
92882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
92903      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.78ms 
92905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
92907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.67ms 
92912      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
96002      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
97006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
97033      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.41ms 
97035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
97035      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.5ns 
97036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
100171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
101193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
101219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.78ms 
101221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
101222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.2ns 
101223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
104323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
105316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
105350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.21ms 
105352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
105352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
105353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
108446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
109413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
109416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
109418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
109418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
109419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
112543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
113542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
113602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.04ms 
113604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
113604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
113605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
116685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
117725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
117820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.95ms 
117824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
117824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.2ns 
117825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
120943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
121938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
122024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.42ms 
122030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
122032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.03ms 
122035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
125170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
126175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
126187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
126189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
126190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.9ns 
126191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
129270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
130294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
130329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.34ms 
130335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
130335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.2ns 
130336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
133435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
134454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
134472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
134476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
134476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.2ns 
134477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
137615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
138588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
138591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
138592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.7ns 
138593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
141717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
142753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
142765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
142768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
142768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 558.6ns 
142771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
145851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
146842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
146852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.24ms 
146854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
146854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
146855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
149920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
150907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
150912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
150914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
150914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
150915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
153986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
154915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
154930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
154931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
154931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
154932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
158015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
159004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
159094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.79ms 
159097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
159097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.2ns 
159101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
162199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
163187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
163216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.9ms 
163222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
163223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 540.31ns 
163224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
166256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
167241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
167268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ms 
167270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
167270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
167271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
170354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
171320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
171347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.96ms 
171349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
171349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
171350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
174437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
175537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
175565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.21ms 
175566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
175567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
175575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
178607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
179592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
179656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.2ms 
179658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
179658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
179659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
182752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
183773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
183783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
183788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
183789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.6ns 
183794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
186962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
187968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
187980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
187983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
187983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.3ns 
187985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
191111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
192137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
192149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
192150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
192150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
192151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
195321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
196388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
196412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
196414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
196414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
196415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
199585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
200631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
200659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.15ms 
200662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
200662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.4ns 
200663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
203863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
204842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
204854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
204855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
204855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
204856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
207934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
208962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
208965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
208967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
208967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
208968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
212097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
213113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
213118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
213120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
213120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
213121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
216207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
217192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
217200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
217202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
217202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176ns 
217203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
220322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
221295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
221415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.98ms 
221418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
221419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.9ns 
221420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
224648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
225680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
225927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 234.45ms 
225931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
225931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.1ns 
225933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
229191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
230276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
230281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
230282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
230282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
230283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
233502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
234518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
234571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.35ms 
234573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
234573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.8ns 
234574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
237813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
238862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
238923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.86ms 
238924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
238924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
238925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
242241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
243281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
243286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
243287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
243287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
243289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
246401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
247400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
247633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 220.42ms 
247636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
247636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321ns 
247637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
250842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
251872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
251890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.29ms 
251891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
251892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.6ns 
251893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
255086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
256079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
256099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
256105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
256106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.3ns 
256109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
259305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
260290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
260315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.09ms 
260317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
260317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
260318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
263428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
264424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
264442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.58ms 
264448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
264449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
264449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
267518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
268541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
268546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
268547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
268547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
268548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
271650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
272611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
272617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
272619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
272619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
272620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
275702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
276677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
276717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ms 
276728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
276729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.6ns 
276730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
279818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
280808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
280834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.44ms 
280835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
280835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
280836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
283913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
284927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
284949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.37ms 
284951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
284951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
284951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
288097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
289061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
289067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
289069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
289069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
289070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
292162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
293167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
293173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
293174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
293175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
293175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
296334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
297322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
297332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
297333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
297333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
297334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
300444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
301467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
301471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
301474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
301474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.1ns 
301475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
304613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
305589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
305592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.7ns 
305593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
305593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
305594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
308737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
309754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
309759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
309762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
309762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.4ns 
309763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
312890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
313883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
313886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
313888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
313888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.4ns 
313889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
317059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
318101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
318183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.82ms 
318185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
318185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
318186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
321367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
322365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
322417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.7ms 
322419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
322421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.79ms 
322422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
325565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
326577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
326629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.63ms 
326632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
326632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
326633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
329836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
330864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
330939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.2ms 
330942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
330942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.5ns 
330943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
334120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
335154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
335201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.34ms 
335202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
335202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
335203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
338393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
339419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
339502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.95ms 
339505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
339505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.3ns 
339506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
342683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
343700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
343743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.54ms 
343746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
343747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.1ns 
343748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
346836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
347880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
347911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.35ms 
347912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
347913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
347913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
351102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
352085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
352119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.78ms 
352120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
352121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
352122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
355260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
356265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
356298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.65ms 
356300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
356300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
356301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
359357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
360353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
360395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.73ms 
360396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
360397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
360397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
363470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
364453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
364492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
364494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
364494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
364497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
367615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
368587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
368631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.53ms 
368633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
368633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157ns 
368634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
371734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
372769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
372828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.95ms 
372832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
372832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.5ns 
372833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
375899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
376922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
376954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ms 
376956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
376956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
376957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
380056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
381060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
381097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.35ms 
381099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
381099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
381100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
384186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
385154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
385191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.64ms 
385193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
385193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
385194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
388271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
389269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
389280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
389282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
389282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
389283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
392366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
393391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
393417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
393420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
393420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
393421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
396477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
397510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
397516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
397517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
397517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
397518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
400667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
401644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
401647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.8ns 
401648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
401648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
401652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
404830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
405839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
405842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.7ns 
405845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
405845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.9ns 
405846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
408902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
409899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
409909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
409910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
409911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
409911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
412959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
413972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
413980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
413982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
413982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
413982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
417091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
418062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
418078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
418079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
418079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
418080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
421157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
422149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
422153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
422155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
422155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
422156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
425193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
426176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
426179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.58ns 
426180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
426180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
426181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
429215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
430197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
430204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
430205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
430205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
430206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
433275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
434237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
434239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.4ns 
434241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
434241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
434242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
437336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
438348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
438350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.8ns 
438353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
438353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns 
438354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
441379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
442363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
442366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.8ns 
442367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
442368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.1ns 
442369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
445425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
446416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
446421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
446422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
446423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
446423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
449504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
450462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
450474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
450475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
450475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
450476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
453617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
454609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
454616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
454618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
454618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
454619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
457653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
458644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
458653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
458654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
458654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
458655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
461753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
462743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
462748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
462750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
462750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
462751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
465802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
466765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
466786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.15ms 
466788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
466788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
466788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
469895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
470914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
470918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
470920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
470920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
470921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
473919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
474913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
474916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
474918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
474918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
474919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
477975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
478963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
478969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
478970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
478970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
478971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
481998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
482955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
482978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.34ms 
482979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
482979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
482980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
486050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
487046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
487053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 741.4ns 
487057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
487057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 
487058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
490096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
491087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
491141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.17ms 
491143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
491143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
491143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
494273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
495246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
495250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
495251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
495251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
495252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
498336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
499344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
499374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.79ms 
499375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
499375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
499376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
502406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
503400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
503428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.22ms 
503431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
503431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
503432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
506529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
507518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
507554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33ms 
507556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
507556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
507557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
510644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
511623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
511628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.4ns 
511629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
511629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
511630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
514732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
515724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
515733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
515735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
515735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
515735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
518882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
519896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
519902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
519905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
519905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.3ns 
519907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
523003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
523997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
524000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
524001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
524001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
524002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
527118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
528124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
528127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
528128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
528129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
528129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
531206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
532195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
532200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
532201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
532201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
532202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
535279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
536265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
536268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
536269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
536270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
536270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
539349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
540312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
540326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.25ms 
540327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
540328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
540328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
543391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
544388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
544407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
544409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
544409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
544410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
547452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
548467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
548483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
548485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
548486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.2ns 
548487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
551571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
552583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
552598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.56ms 
552601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
552601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
552602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
555695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
556705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
556712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
556714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
556714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.7ns 
556715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
559825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
560838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
560846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
560847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
560847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
560848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
563900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
564926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
564931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
564932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
564932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
564933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
568019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
569019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
569022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
569024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
569024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
569025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
572099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
573090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
573093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
573094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
573094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
573095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
576159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
577160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
577174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
577176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
577176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
577176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
580337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
581350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
581355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
581357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
581357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
581358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
584396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
585411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
585420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
585422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
585422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
585423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
588538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
589547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
589549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.9ns 
589551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
589551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
589551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
592643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
593640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
593643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.8ns 
593644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
593644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
593645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
596732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
597749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
597754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
597756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
597756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
597757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
600858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
601882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
601885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
601887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
601887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
601887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
604960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
605961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
605965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
605966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
605966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
605967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
609060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
610053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
610057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
610058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
610059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
610059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
613168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
614169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
614176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
614177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
614177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
614178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
617213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
618210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
618213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
618215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
618215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
618215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
621310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
622331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
622345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
622347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
622347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
622348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
625428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
626462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
626464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.9ns 
626466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
626466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
626467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
629579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
630597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
630607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
630608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
630608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
630609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
633770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
634782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
634785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
634786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
634786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
634787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
637904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
638972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
638975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
638977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
638977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
638977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
642197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
643236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
643243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
643245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
643245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
643246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
646324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
647342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
647346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
647348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
647348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
647348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
650415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
651427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
651431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
651433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
651433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
651433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
654530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
655539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
655544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
655545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
655545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
655546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
658648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
659639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
659646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
659647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
659647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
659648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
662763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
663782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
663802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.08ms 
663804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
663804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
663805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
666996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
668010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
668034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.22ms 
668035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
668036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
668036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
671130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
672149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
672163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.32ms 
672164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
672164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
672165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
675281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
676321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
676335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
676337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
676337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
676337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
679444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
680466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
680501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.72ms 
680503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
680503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
680504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
683677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
684743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
684780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.09ms 
684782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
684782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
684783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
687990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
689028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
689061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30ms 
689062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
689062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
689063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
692248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
693266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
693285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.82ms 
693286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
693287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
693287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
696419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
697416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
697460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.88ms 
697462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
697462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
697462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
700607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
701622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
701695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.12ms 
701697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
701697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
701698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
704777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
705801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
705857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.86ms 
705859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
705859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
705860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
708929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
709942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
710001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.51ms 
710003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
710003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
710004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
713126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
714126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
714189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.29ms 
714191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
714191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
714192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
717272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
718295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
718464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 160.95ms 
718467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
718467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.4ns 
718468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
721576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
722592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
722602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.13ms 
722604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
722604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
722605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
725661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
726678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
726688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
726689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
726690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
726690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
729762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
730772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
730779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
730780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
730780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
730781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
733846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
734851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
734876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
734877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
734877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
734878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
737925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
738915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
738930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
738933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
738933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
738934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
742028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
743046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
743050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
743051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
743052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.6ns 
743053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
746179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
747202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
747226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.04ms 
747227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
747227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
747228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
750326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
751330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
751355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.44ms 
751357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
751357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
751358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
754450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
755447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
755477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.96ms 
755478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
755478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
755479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
758550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
759578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
759585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
759586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
759586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
759587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
762694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
763747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
763755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
763760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
763760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
763761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
766868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
767876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
767884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
767885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
767885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
767886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
770990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
772037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
772046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.76ms 
772048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
772048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
772049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
775173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
776194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
776297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.41ms 
776298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
776298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
776299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
779445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
780465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
780507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.95ms 
780510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
780510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.9ns 
780511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
783579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
784595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
784626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.77ms 
784628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
784628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
784629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
787675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
788697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
788699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.2ns 
788701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
788701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
788702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
791819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
792840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
793118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 264.97ms 
793120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
793120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.3ns 
793121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
796284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
797306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
797377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.22ms 
797378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
797378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
797379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
800525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
801547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
801550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 388.9ns 
801551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
801551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
801552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
804715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
805726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
805728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432.7ns 
805730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
805730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
805731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
808785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
809807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
809809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 506.6ns 
809810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
809810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
809811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
812919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
813936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
813939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.6ns 
813940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
813940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
813941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
817039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
818046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
818182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 133.7ms 
818185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
818185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281ns 
818186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
821335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
822340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
822398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.92ms 
822399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
822399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
822405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
825470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
826531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
826533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
826570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
826627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
826657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
826666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
826681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
826685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
826687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
826691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
826698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
826701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
826706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
826709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
826979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
826981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
826982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
826988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
826989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
827127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
827133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
827134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
827136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
827137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
827138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
827337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
827339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
827340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
827341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
827342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
827344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
827519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
827521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
827529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
827530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
827532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
827533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
827540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
827542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
827543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
827545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
827546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
827547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
827556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
827558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
827559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
827560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
827561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
827562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
827712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
827714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
827715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
827853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
827856     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)'' 
827858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
827860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
827861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
827862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
827863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
827864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
827872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
827874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
827875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
827876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
827877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
828008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
828012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
828014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
828015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
828018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
828019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
828021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
828162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
828164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
828165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
828166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
828167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
828168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
828169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
828170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
828286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
828288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
828401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
828407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
828413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
828414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
828415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
828417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
828418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
828418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
828419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
828421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
828431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
828437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
828569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
828571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
828572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
828573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
828574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
828575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
828576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
828577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
828638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
828644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
828757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
828759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
828761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
828763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
828764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
828765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
828924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
828930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
828932     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)'' 
828934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
828935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
828936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
828936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
828937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
828949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
828951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
828952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
828962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
829093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
829095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
829096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
829097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
829098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
829100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
829243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
829245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
829246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
829247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
829249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
829250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
829250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
829252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
829362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
829364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
829461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
829461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
829462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
829468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
829473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
829479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
829631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
829634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
829635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
829636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
829649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
829753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
834255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
834256     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)'' 
834263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
834264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
834265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
834266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
834266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
834281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
834283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
834284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
834285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
834286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
834406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
834411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
834412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
834413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
834413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
834414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
834415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
834541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
834543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
834543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
834546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
834547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
834547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
834549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
834550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
834650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
834652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
834741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
834747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
834752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
834753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
834754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
834755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
834818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
834922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
834923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
834924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
834925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
835017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
835028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
835029     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)'' 
835031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
835032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
835032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
835033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
835034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
835046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
835048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
835049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
835049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
835050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
835161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
835163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
835164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
835165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
835165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
835276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
835282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
835283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
835284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
835284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
835285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
835286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
835410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
835411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
835412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
835413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
835414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
835414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
835415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
835416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
835417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
835417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
835419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
835419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
835420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
835420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
835421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
835526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
835528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
835535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
835629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
835733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
835735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
835736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
835736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
835737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
835738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
835738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
835738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
835740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
835853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
835861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
835971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
835972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
835973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
835974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
835974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
835975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
835975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
835976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
835982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
835984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
836085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
836091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
836099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
836227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
836229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
836229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
836231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
836231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
836231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
836232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
836233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
836310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
836312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
836313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
836313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
836315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
836322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
836329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
836471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
836588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
836592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
836594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
836595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
836807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
836966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
836967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
840686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
840692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
840693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
840694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
840694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
840834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
840836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
840837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
840838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
840838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
841016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
844697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
848630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
848637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
848638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
848639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
848642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
848788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
848790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
848791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
848792     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)' ...' 
848794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
850225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
850225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
850226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
853502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
854532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
854534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
854535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
854545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
854558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
854561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
854563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
854563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
854569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
854570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
854575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
854578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
854579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
854590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
854592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
854592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
854648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
854649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
854650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
854650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
854651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
854747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
854747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
854749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
854750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
854750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
854754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
854755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
854755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
854756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
854757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
854758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
854875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
854876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
854877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
854878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
854879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
854879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
854989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
854990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
854990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
854991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
854991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
854993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
854993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
854993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
854994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
854995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
854995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
854995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
854996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
854996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
854997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
854997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
854998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
854999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
855000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
855003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
855056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
855058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
855132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
855133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
855135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
855136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
855137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
855137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
855200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
855202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
855203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
855205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
855206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
855207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
855207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
855268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
855270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
855274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
855333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
855397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
855397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
855398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
858570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
859653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
859718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.31ms