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

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

tests
0

failures
0

ignored
14m0.80s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.985s passed
powPositiveConcrete data()[101] 3.870s passed
powGeq1Concrete data()[102] 3.898s passed
pow2InIntLower data()[103] 3.907s passed
pow2InIntUpper data()[104] 3.973s passed
logSelfConcrete data()[105] 3.975s passed
log1Concrete data()[106] 3.996s passed
logProduct data()[107] 3.878s passed
logTimesBaseConcrete data()[108] 3.753s passed
logProdIdentity data()[109] 3.823s passed
moduloByteIsInByte data()[10] 4.082s passed
logProdIdentityConcrete data()[110] 3.841s passed
logPowIdentity data()[111] 3.795s passed
logPowIdentityConcrete data()[112] 3.993s passed
logPositive data()[113] 4.081s passed
logPositiveConcrete data()[114] 4.311s passed
logMono data()[115] 4.106s passed
logMonoConcrete data()[116] 4.203s passed
powLogLess data()[117] 4.158s passed
powLogMore2 data()[118] 4.193s passed
logLessThanPow data()[119] 4.219s passed
moduloCharIsInChar data()[11] 4.149s passed
logLessThanPowConcrete data()[120] 4.242s passed
logSqueeze data()[121] 4.202s passed
ifthenelse_equals data()[122] 4.140s passed
ifthenelse_equals_1 data()[123] 4.029s passed
ifthenelse_equals_2 data()[124] 4.117s passed
disjointWithSingleton1 data()[125] 4.135s passed
disjointWithSingleton2 data()[126] 4.214s passed
disjointArrayRanges data()[127] 4.217s passed
disjointArrayRangeAllFields1 data()[128] 4.232s passed
disjointArrayRangeAllFields2 data()[129] 4.127s passed
div_unique1 data()[12] 4.029s passed
seqSelfDefinition data()[130] 4.173s passed
seqOutsideValue data()[131] 4.140s passed
castedGetAny data()[132] 4.232s passed
seqGetAlphaCast data()[133] 4.248s passed
getOfSeqSingleton data()[134] 4.233s passed
getOfSeqSingletonConcrete data()[135] 4.265s passed
getOfSeqConcat data()[136] 4.242s passed
getOfSeqSub data()[137] 4.179s passed
getOfSeqReverse data()[138] 4.165s passed
lenOfSeqEmpty data()[139] 4.279s passed
div_unique2 data()[13] 3.939s passed
lenOfSeqSingleton data()[140] 4.159s passed
lenOfSeqConcat data()[141] 4.229s passed
lenOfSeqSub data()[142] 4.222s passed
lenOfSeqReverse data()[143] 4.224s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.178s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.208s passed
getOfSeqSingletonEQ data()[146] 4.340s passed
getOfSeqConcatEQ data()[147] 4.260s passed
getOfSeqSubEQ data()[148] 4.301s passed
getOfSeqReverseEQ data()[149] 4.247s passed
div_exists data()[14] 4.022s passed
lenOfSeqEmptyEQ data()[150] 4.362s passed
lenOfSeqSingletonEQ data()[151] 4.355s passed
lenOfSeqConcatEQ data()[152] 4.274s passed
lenOfSeqSubEQ data()[153] 4.366s passed
lenOfSeqReverseEQ data()[154] 4.259s passed
getOfSeqDefEQ data()[155] 4.185s passed
lenOfSeqDefEQ data()[156] 4.222s passed
seqConcatWithSeqEmpty1 data()[157] 4.287s passed
seqConcatWithSeqEmpty2 data()[158] 4.240s passed
seqReverseOfSeqEmpty data()[159] 4.202s passed
div_one data()[15] 3.849s passed
subSeqComplete data()[160] 4.228s passed
subSeqTailR data()[161] 4.088s passed
subSeqTailL data()[162] 4.162s passed
subSeqTailEQR data()[163] 4.240s passed
subSeqTailEQL data()[164] 4.211s passed
seqDef_split data()[165] 4.270s passed
seqDef_induction_upper data()[166] 4.355s passed
seqDef_induction_upper_concrete data()[167] 4.293s passed
seqDef_induction_lower data()[168] 4.293s passed
seqDef_induction_lower_concrete data()[169] 4.281s passed
jdiv_one data()[16] 3.758s passed
seqDef_split_in_three data()[170] 4.377s passed
seqDef_empty data()[171] 4.113s passed
seqDef_one_summand data()[172] 4.250s passed
seqDef_lower_equals_upper data()[173] 4.234s passed
seqDefOfSeq data()[174] 4.246s passed
seqSelfDefinitionEQ2 data()[175] 4.183s passed
indexOfSeqSingleton data()[176] 4.202s passed
indexOfSeqConcatFirst data()[177] 4.250s passed
indexOfSeqConcatSecond data()[178] 4.171s passed
indexOfSeqSub data()[179] 4.175s passed
div_zero data()[17] 3.846s passed
lenOfArray2seq data()[180] 4.153s passed
getAnyOfArray2seq data()[181] 4.161s passed
getOfArray2seq data()[182] 4.221s passed
getAnyOfNPermInv data()[183] 4.136s passed
seqNPermRange data()[184] 4.415s passed
seqPermTrans data()[185] 4.278s passed
seqPermRefl data()[186] 4.222s passed
seqPermSplit data()[187] 4.156s passed
seqNPermRight data()[188] 4.449s passed
seqPermFromSwap data()[189] 4.342s passed
divResZero1 data()[18] 3.937s passed
seqPermTransAlt0 data()[190] 4.208s passed
seqPermTransAlt1 data()[191] 4.353s passed
seqPermTransAlt2 data()[192] 4.155s passed
seqPermTransAlt3 data()[193] 4.014s passed
seqPermForall data()[194] 4.269s passed
seqPermExists data()[195] 4.244s passed
schiffl_lemma_2 data()[196] 28.476s passed
schiffl_thm_1 data()[197] 5.270s passed
eqSameSeq data()[198] 4.297s passed
divResZero2 data()[19] 3.982s passed
eqTermCut data()[1] 5.087s passed
divResOne1 data()[20] 4.144s passed
divResOne2 data()[21] 4.040s passed
div_cancel1 data()[22] 4.030s passed
div_cancel2 data()[23] 4.082s passed
divAddMultDenom data()[24] 4.086s passed
divMinus data()[25] 4.119s passed
divMinusDenom data()[26] 4.030s passed
divLeastDPos data()[27] 3.911s passed
divLeastDNeg data()[28] 3.968s passed
divGreatestDPos data()[29] 3.841s passed
equivAllRight data()[2] 4.517s passed
divGreatestDNeg data()[30] 3.892s passed
divIncreasingPos data()[31] 3.889s passed
divIncreasingNeg data()[32] 3.888s passed
jdiv_zero data()[33] 3.969s passed
jdivPulloutMinusNum data()[34] 4.150s passed
jdivPulloutMinusDenom data()[35] 4.492s passed
jdiv_uniquePosPos data()[36] 4.101s passed
jdiv_uniquePosNeg data()[37] 4.184s passed
jdiv_uniqueNegPos data()[38] 4.046s passed
jdiv_uniqueNegNeg data()[39] 3.950s passed
irrflConcrete1 data()[3] 4.776s passed
jdivMultDenom1 data()[40] 4.194s passed
jdivMultDenom2 data()[41] 4.187s passed
mod_geZero data()[42] 4.012s passed
mod_lessDenom data()[43] 4.007s passed
jmod_NumPos data()[44] 4.005s passed
jmod_NumNeg data()[45] 4.144s passed
jmod_geZero data()[46] 4.004s passed
jmodNumZero data()[47] 4.026s passed
jmod_pulloutminusNum data()[48] 4.105s passed
jmod_pulloutminusDenom data()[49] 4.008s passed
irrflConcrete2 data()[4] 4.354s passed
jmodUnique1 data()[50] 4.199s passed
jmodUnique2 data()[51] 4.186s passed
intDivRem data()[52] 4.072s passed
jmodjmod data()[53] 4.109s passed
jmodDivisible data()[54] 4.152s passed
jmodDivisibleRep data()[55] 4.118s passed
jdivAddMultDenom data()[56] 4.160s passed
jmodAltZero data()[57] 4.009s passed
jmodAddMultDenomZero data()[58] 3.936s passed
polyDiv_zero data()[59] 3.973s passed
cancel_gtPos data()[5] 4.581s passed
polyMod_ltdivDenom data()[60] 4.113s passed
bsum_empty data()[61] 4.019s passed
bsum_induction_upper data()[62] 4.089s passed
bsum_induction_lower data()[63] 4.131s passed
bsum_num_of_bounds data()[64] 4.087s passed
bsum_num_of_bounds2 data()[65] 4.000s passed
bsum_induction_upper2 data()[66] 3.961s passed
bsum_induction_upper_concrete data()[67] 3.903s passed
bsum_induction_upper_concrete_2 data()[68] 3.891s passed
bsum_induction_upper2_concrete data()[69] 3.905s passed
cancel_gtNeg data()[6] 4.395s passed
bsum_induction_lower_concrete data()[70] 3.956s passed
bsum_induction_lower2 data()[71] 3.967s passed
bsum_induction_lower2_concrete data()[72] 3.986s passed
bsum_positive data()[73] 4.018s passed
bsum_upper_bound data()[74] 4.012s passed
bsum_lower_bound data()[75] 4.013s passed
bsum_positive_lower_bound_element data()[76] 4.028s passed
bsum_sub_same_index data()[77] 4.006s passed
bsum_less_same_index data()[78] 3.952s passed
bsum_equal_except_one_index data()[79] 3.963s passed
moduloIntIsInInt data()[7] 4.185s passed
bsum_num_of_is_max data()[80] 3.915s passed
bsum_num_of_is_max2 data()[81] 3.834s passed
bsum_num_of_is_max3 data()[82] 3.778s passed
bsum_num_of_is_max4 data()[83] 3.789s passed
bsum_num_of_lt_max data()[84] 3.837s passed
bsum_num_of_lt_max2 data()[85] 3.898s passed
bsum_num_of_lt_max3 data()[86] 3.799s passed
bsum_num_of_lt_max4 data()[87] 3.985s passed
bsum_num_of_gt0 data()[88] 3.968s passed
bsum_num_of_gt0_alt data()[89] 4.077s passed
moduloLongIsInLong data()[8] 4.139s passed
bsum_add_concrete data()[90] 4.025s passed
bprod_all_positive data()[91] 3.963s passed
bprod_split data()[92] 3.953s passed
powConcrete0 data()[93] 4.029s passed
powConcrete1 data()[94] 4.031s passed
powSplitFactor data()[95] 4.023s passed
powAdd data()[96] 4.219s passed
powMono data()[97] 4.056s passed
powMonoConcrete data()[98] 4.089s passed
powMonoConcreteRight data()[99] 4.023s passed
moduloShortIsInShort data()[9] 4.133s passed

Standard output

681        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
714        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 14.71ms 
1072       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1094       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)

2374       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2377       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2381       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2381       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3946       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.64s 
10798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.8ns 
10858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 550.19ns 
10873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
14674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15932      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.76ms 
15952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 851.09ns 
15957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19445      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
19445      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20466      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.89ms 
20469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20470      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.1ns 
20473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
24027      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
25245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.7ns 
25246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
28540      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
29599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 578.99ns 
29601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
32962      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34174      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.78ms 
34183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34184      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 676.19ns 
34186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
37491      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38573      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.52ms 
38577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.09ns 
38579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
41755      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.19ns 
42763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.7ns 
42764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
45894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46896      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.59ns 
46902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.1ns 
46910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50032      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
50032      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
51033      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.89ns 
51035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
51036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.39ns 
51037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
54134      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55115      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.59ns 
55118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.89ns 
55120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
58273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
59264      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.29ns 
59267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
59267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385ns 
59268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
62270      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.98ms 
63298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 628.99ns 
63303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
66192      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.8ms 
67237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.9ns 
67239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
70132      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71257      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.24ms 
71261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.8ns 
71262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
74207      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75107      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
75111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.7ns 
75112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
77950      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
78862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
78866      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
78870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
78870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.9ns 
78872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
81714      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
82649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
82712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.57ms 
82716      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
82717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns 
82718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85657      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
85658      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
86626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
86651      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.43ms 
86653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
86653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
86654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
89643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
90611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
90633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ms 
90635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
90635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
90636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
93755      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
94752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
94777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
94780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
94780      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.5ns 
94782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
97823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
98795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
98817      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.8ms 
98822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
98822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.8ns 
98823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
101841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
102812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
102848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.78ms 
102850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
102850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.3ns 
102851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
105886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
106926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
106930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
106931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
106932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
106933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
109942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
110940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
111014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.57ms 
111019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
111020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.8ns 
111021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
114077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
115050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
115135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.74ms 
115138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
115138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
115139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
118172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
119096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
119166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.91ms 
119168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
119168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
119169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
122147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
123065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
123076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.62ms 
123080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
123081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395ns 
123082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
126068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
127022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
127045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.41ms 
127053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
127053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
127055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
129971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
130878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
130893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
130894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
130894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
130895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
133821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
134773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
134784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
134787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
134788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.2ns 
134789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
137721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
138662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
138674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
138677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
138677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320ns 
138678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
141562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
142552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
142562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.96ms 
142564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
142564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
142565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
145608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
146525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
146531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
146533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
146533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
146534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
149674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
150663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
150680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 
150684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
150684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.6ns 
150686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
154075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
155099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
155173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.02ms 
155176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
155176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.2ns 
155178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
158273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
159249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
159275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
159277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
159277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
159279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
162443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
163431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
163459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms 
163461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
163461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 
163462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
166456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
167474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
167504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.95ms 
167507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
167507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.1ns 
167509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
170535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
171431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
171455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.97ms 
171457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
171457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 
171458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
174619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
175588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
175649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.15ms 
175652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
175652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.9ns 
175655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
178826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
179827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
179835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
179838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
179838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
179840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
182887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
183841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
183847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
183850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
183850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.6ns 
183852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
186852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
187844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
187855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.58ms 
187857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
187857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
187858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
190856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
191847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
191860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
191861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
191862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
191863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
194973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
195958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
196004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.08ms 
196011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
196011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 
196012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
199055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
199996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
200008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.34ms 
200010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
200010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
200011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
203071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
204029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
204034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
204036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
204036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.7ns 
204037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
207145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
208134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
208139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
208141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
208141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
208142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
211161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
212141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
212147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
212149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
212149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.1ns 
212150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
215257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
216244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
216346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.32ms 
216348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
216348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.4ns 
216350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
219407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
220413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
220531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.98ms 
220541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
220548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.64ms 
220550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
223662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
224599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
224604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
224607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
224608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.5ns 
224609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
227677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
228655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
228713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.52ms 
228716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
228716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.49ns 
228718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
231817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
232822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
232866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.53ms 
232868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
232868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
232869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
235966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
236977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
236984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
236989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
236989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
236990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
239977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
240941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
241146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.44ms 
241149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
241149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312ns 
241151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
244197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
245142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
245156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
245157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
245157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
245158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
248166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
249082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
249093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
249094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
249094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
249095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
252068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
253043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
253064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
253067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
253067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.8ns 
253068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
256149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
257161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
257177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
257180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
257180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
257181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
260219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
261192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
261197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
261199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
261199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 
261200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
264202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
265281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
265287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
265288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
265288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
265289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
268380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
269385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
269417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.91ms 
269419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
269419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns 
269420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
272471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
273482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
273504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.38ms 
273506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
273506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
273507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
276548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
277483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
277504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.74ms 
277506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
277507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.8ns 
277508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
280521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
281461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
281466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
281467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
281467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
281468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
284387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
285362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
285368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
285370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
285370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
285371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
288291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
289250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
289259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
289262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
289262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256ns 
289263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
292214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
293161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
293165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
293166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
293167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 
293167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
296185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
297117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
297121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.49ns 
297123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
297123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.8ns 
297124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
300131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
301083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
301088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
301090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
301090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
301091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
304111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
305071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
305075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
305076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
305076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
305077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
308053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
309018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
309092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.02ms 
309094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
309094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
309095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
312085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
313039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
313103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.91ms 
313105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
313105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
313106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
316099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
317066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
317117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.11ms 
317120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
317120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.4ns 
317121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
320116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
321074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
321145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.05ms 
321147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
321148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
321149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
324207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
325109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
325151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.32ms 
325153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
325153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
325154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
328053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
329031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
329103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.58ms 
329105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
329105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.1ns 
329106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
332049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
333030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
333066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.74ms 
333068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
333068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
333069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
336016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
336953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
336981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.05ms 
336983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
336983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
336984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
339824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
340782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
340815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.71ms 
340817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
340817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
340818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
343663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
344566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
344593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
344595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
344595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
344596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
347464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
348343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
348382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.38ms 
348384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
348384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
348384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
351260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
352184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
352219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.69ms 
352221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
352221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
352222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
355155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
356080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
356117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.57ms 
356119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
356119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.6ns 
356120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
358959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
359882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
359916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.61ms 
359917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
359917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
359918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
362910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
363870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
363901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.7ms 
363903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
363903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
363903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
366911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
367834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
367869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.51ms 
367871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
367871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
367871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
370935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
371909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
371946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.73ms 
371947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
371948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
371949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
374986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
375961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
375971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
375972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
375973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
375973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
378930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
379908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
379934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.31ms 
379936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
379936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
379937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
382901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
383882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
383888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
383889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
383889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
383890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
386890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
387913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
387917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
387918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
387918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
387919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
390979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
391944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
391948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
391949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
391949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
391950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
395029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
395960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
395970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
395972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
395972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
395973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
399181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
400180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
400189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
400191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
400191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.6ns 
400193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
403226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
404225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
404245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.09ms 
404246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
404247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
404247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
407300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
408330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
408334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
408336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
408336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
408337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
411391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
412354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
412357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.99ns 
412359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
412359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns 
412360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
415377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
416335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
416342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
416343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
416343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
416344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
419292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
420210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
420213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 796.89ns 
420214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
420214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
420215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
423165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
424108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
424110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.69ns 
424112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
424112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
424113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
427073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
428015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
428017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.89ns 
428019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
428019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
428020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
431013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
431985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
431991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
431992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
431992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
431993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
434988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
435954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
435965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
435966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
435967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
435967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
438983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
439956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
439961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
439963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
439963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
439964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
442899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
443829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
443839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
443840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
443840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
443841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
446719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
447587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
447592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
447593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
447594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
447594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
450473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
451394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
451415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.19ms 
451417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
451417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
451418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
454299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
455250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
455257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
455258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
455258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
455259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
458076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
459047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
459052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
459053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
459053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
459054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
462074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
463036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
463044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
463045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
463045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
463046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
466070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
467093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
467125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.46ms 
467128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
467128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
467129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
470433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
471431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
471437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
471440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
471440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
471441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
474481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
475482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
475543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.09ms 
475545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
475545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
475546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
478747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
479742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
479747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
479749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
479749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
479750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
482816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
483870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
483904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.33ms 
483907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
483907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.7ns 
483909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
487069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
488062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
488098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.99ms 
488100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
488100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
488100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
491270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
492281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
492317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.98ms 
492319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
492319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
492320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
495555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
496555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
496559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.09ns 
496562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
496562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 
496563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
499723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
500753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
500761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
500763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
500763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
500764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
503925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
504897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
504901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
504903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
504903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
504904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
507889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
508927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
508930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
508932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
508932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
508933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
512032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
513045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
513048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
513049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
513049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
513050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
516194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
517178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
517183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
517184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
517184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
517185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
520349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
521393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
521396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
521398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
521398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
521399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
524533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
525597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
525613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.59ms 
525615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
525615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
525616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
528812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
529825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
529845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.17ms 
529847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
529847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
529848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
532963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
533948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
533970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.87ms 
533975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
533975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.8ns 
533976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
537124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
538128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
538145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
538147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
538147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
538148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
541239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
542279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
542285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
542286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
542286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
542288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
545498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
546506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
546516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
546519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
546519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
546520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
549715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
550762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
550765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 956.89ns 
550767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
550767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
550768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
553943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
554994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
554998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
555000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
555000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
555001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
558256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
559260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
559264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
559265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
559265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
559266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
562458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
563490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
563505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
563507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
563508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.1ns 
563509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
566649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
567678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
567684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
567686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
567686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
567686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
570831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
571840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
571849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
571851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
571851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
571852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
575061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
576125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
576128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 921.19ns 
576130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
576130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
576131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
579257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
580284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
580287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.39ns 
580289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
580289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
580289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
583483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
584511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
584516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
584518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
584518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
584519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
587671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
588734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
588738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
588739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
588739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
588740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
591941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
592957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
592962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
592964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
592964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
592965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
596065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
597137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
597140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
597142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
597142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
597143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
600302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
601341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
601348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
601350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
601350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
601351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
604649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
605683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
605688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
605690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
605691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281ns 
605691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
608834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
609932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
609948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
609949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
609950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.3ns 
609950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
613216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
614246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
614250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.99ns 
614251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
614251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
614252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
617451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
618486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
618496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
618498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
618498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
618499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
621779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
622856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
622859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
622860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
622860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
622861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
626139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
627210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
627214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
627215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
627215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
627216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
630468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
631481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
631487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
631489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
631489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
631490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
634768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
635846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
635853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
635854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
635854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
635855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
639042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
640108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
640113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
640114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
640114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
640115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
643279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
644293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
644298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
644299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
644299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
644300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
647454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
648512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
648519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
648521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
648521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
648522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
651733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
652786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
652806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
652807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
652808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
652808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
655978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
657024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
657046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.44ms 
657048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
657048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
657049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
660212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
661235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
661249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
661250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
661250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
661251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
664477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
665460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
665476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
665477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
665478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
665478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
668523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
669528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
669564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.95ms 
669565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
669566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
669566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
672670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
673691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
673726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.41ms 
673728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
673728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
673729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
676896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
677922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
677966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.24ms 
677967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
677967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
677968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
681121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
682157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
682177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.61ms 
682179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
682179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
682180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
685386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
686401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
686446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.89ms 
686449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
686450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.4ns 
686451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
689704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
690731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
690802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.1ms 
690804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
690804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
690805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
693960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
695038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
695095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.83ms 
695096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
695096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
695097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
698252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
699328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
699388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.58ms 
699390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
699390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
699391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
702561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
703600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
703669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.5ms 
703671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
703671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns 
703672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
706815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
707872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
708046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 165.98ms 
708047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
708048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
708048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
711126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
712148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
712159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 
712161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
712161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
712162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
715375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
716396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
716408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ms 
716411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
716411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.2ns 
716413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
719602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
720636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
720643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
720645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
720645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
720646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
723818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
724862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
724889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
724891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
724891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
724892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
728031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
729056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
729072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
729074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
729074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
729075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
732254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
733270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
733274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
733276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
733276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
733277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
736467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
737499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
737524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.87ms 
737525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
737525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
737526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
740656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
741672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
741696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.42ms 
741697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
741697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
741698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
744804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
745831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
745870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.32ms 
745871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
745871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
745872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
749002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
750019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
750024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
750025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
750025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
750026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
753161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
754179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
754184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
754185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
754185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
754186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
757338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
758362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
758405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.32ms 
758407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
758407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.6ns 
758408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
761502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
762531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
762541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
762543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
762543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
762544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
765775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
766839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
766956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.53ms 
766958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
766959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.3ns 
766960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
770138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
771188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
771234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.27ms 
771236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
771236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 
771237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
774381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
775425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
775456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.17ms 
775458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
775458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
775458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
778587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
779610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
779613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 480.9ns 
779614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
779614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
779616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
782735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
783757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
784061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.81ms 
784064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
784064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286ns 
784065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
787280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
788328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
788403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.39ms 
788405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
788405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
788406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
791553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
792609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
792612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 434.1ns 
792613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
792613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
792614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
795932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
796962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
796964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.3ns 
796966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
796966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
796967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
800099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
801117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
801120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.5ns 
801121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
801121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
801122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
804134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
805131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
805133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650ns 
805135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
805135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
805135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
808209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
809274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
809402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 124.83ms 
809404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
809405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.7ns 
809407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
812505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
813574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
813646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.34ms 
813648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
813648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
813657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
816803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
817812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
817813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
817858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
817920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
817952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
817960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
817971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
817974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
817975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
817979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
817983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
817986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
817991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
817992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
818287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
818289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
818291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
818292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
818293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
818435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
818437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
818438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
818440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
818441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
818442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
818673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
818675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
818676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
818677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
818678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
818680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
818858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
818860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
818861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
818861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
818862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
818863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
818871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
818872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
818873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
818876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
818877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
818878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
818885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
818886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
818888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
818889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
818890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
818891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
819039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
819040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
819042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
819177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
819179     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)'' 
819182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
819183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
819185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
819186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
819187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
819188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
819197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
819200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
819201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
819202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
819203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
819347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
819351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
819353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
819354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
819355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
819356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
819357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
819491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
819493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
819494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
819496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
819497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
819498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
819498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
819500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
819601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
819603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
819715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
819721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
819726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
819728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
819729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
819730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
819731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
819731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
819732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
819733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
819745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
819751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
819864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
819866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
819867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
819869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
819869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
819870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
819871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
819872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
819931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
819938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
820042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
820045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
820047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
820049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
820050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
820051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
820196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
820202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
820203     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)'' 
820205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
820207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
820208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
820215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
820216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
820227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
820229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
820230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
820231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
820342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
820345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
820345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
820347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
820350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
820351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
820473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
820475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
820477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
820478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
820479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
820480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
820480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
820482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
820586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
820589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
820697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
820698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
820699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
820706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
820712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
820717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
820877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
820879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
820880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
820881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
820895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
821002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
825786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
825787     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)'' 
825794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
825795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
825796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
825797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
825797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
825808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
825810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
825811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
825812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
825813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
825934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
825938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
825940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
825941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
825941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
825942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
825943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
826070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
826071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
826072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
826073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
826074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
826074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
826075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
826076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
826175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
826177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
826270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
826275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
826279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
826281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
826282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
826283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
826295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
826404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
826405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
826406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
826407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
826504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
826516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
826517     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)'' 
826519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
826520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
826521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
826521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
826522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
826535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
826537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
826538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
826538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
826539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
826653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
826655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
826656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
826657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
826658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
826781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
826787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
826788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
826789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
826789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
826790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
826791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
826920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
826921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
826922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
826924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
826924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
826925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
826925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
826926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
826927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
826928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
826929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
826930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
826930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
826931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
826932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
827048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
827049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
827124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
827229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
827336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
827338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
827340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
827341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
827342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
827343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
827343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
827344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
827345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
827457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
827465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
827583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
827585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
827586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
827587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
827588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
827588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
827589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
827589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
827595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
827596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
827701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
827707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
827713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
827843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
827844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
827845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
827846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
827847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
827847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
827848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
827848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
827920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
827922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
827922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
827923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
827924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
827930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
827936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
828086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
828200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
828201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
828202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
828203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
828410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
828523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
828524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
832349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
832354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
832355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
832356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
832357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
832497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
832498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
832500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
832500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
832501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
832633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
836549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
840528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
840533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
840534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
840535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
840536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
840736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
840737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
840738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
840739     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)' ...' 
840741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
842123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
842124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.2ns 
842125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
845433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
846494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
846495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
846496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
846508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
846525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
846528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
846530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
846530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
846536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
846538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
846543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
846546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
846546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
846559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
846562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
846563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
846634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
846646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
846646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
846647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
846648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
846737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
846738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
846740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
846741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
846741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
846747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
846748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
846748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
846750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
846751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
846751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
846863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
846864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
846865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
846866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
846867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
846868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
846976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
846978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
846978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
846979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
846980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
846981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
846982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
846983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
846984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
846984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
846985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
846985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
846986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
846987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
846988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
846989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
846989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
846991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
846992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
846995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
847044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
847046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
847119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
847120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
847122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
847124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
847124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
847125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
847189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
847192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
847194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
847195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
847197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
847197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
847198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
847253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
847256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
847260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
847325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
847394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
847394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.5ns 
847395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
850563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
851646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
851689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.45ms