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

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

tests
0

failures
0

ignored
10m40.93s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.098s passed
powPositiveConcrete data()[101] 3.081s passed
powGeq1Concrete data()[102] 3.096s passed
pow2InIntLower data()[103] 3.093s passed
pow2InIntUpper data()[104] 3.075s passed
logSelfConcrete data()[105] 3.094s passed
log1Concrete data()[106] 3.075s passed
logProduct data()[107] 3.098s passed
logTimesBaseConcrete data()[108] 3.091s passed
logProdIdentity data()[109] 3.101s passed
moduloByteIsInByte data()[10] 3.163s passed
logProdIdentityConcrete data()[110] 3.075s passed
logPowIdentity data()[111] 3.099s passed
logPowIdentityConcrete data()[112] 3.090s passed
logPositive data()[113] 3.088s passed
logPositiveConcrete data()[114] 3.091s passed
logMono data()[115] 3.102s passed
logMonoConcrete data()[116] 3.091s passed
powLogLess data()[117] 3.108s passed
powLogMore2 data()[118] 3.087s passed
logLessThanPow data()[119] 3.108s passed
moduloCharIsInChar data()[11] 3.174s passed
logLessThanPowConcrete data()[120] 3.088s passed
logSqueeze data()[121] 3.096s passed
ifthenelse_equals data()[122] 3.090s passed
ifthenelse_equals_1 data()[123] 3.094s passed
ifthenelse_equals_2 data()[124] 3.093s passed
disjointWithSingleton1 data()[125] 3.078s passed
disjointWithSingleton2 data()[126] 3.087s passed
disjointArrayRanges data()[127] 3.094s passed
disjointArrayRangeAllFields1 data()[128] 3.096s passed
disjointArrayRangeAllFields2 data()[129] 3.095s passed
div_unique1 data()[12] 3.202s passed
seqSelfDefinition data()[130] 3.099s passed
seqOutsideValue data()[131] 3.099s passed
castedGetAny data()[132] 3.105s passed
seqGetAlphaCast data()[133] 3.102s passed
getOfSeqSingleton data()[134] 3.097s passed
getOfSeqSingletonConcrete data()[135] 3.097s passed
getOfSeqConcat data()[136] 3.106s passed
getOfSeqSub data()[137] 3.093s passed
getOfSeqReverse data()[138] 3.095s passed
lenOfSeqEmpty data()[139] 3.117s passed
div_unique2 data()[13] 3.189s passed
lenOfSeqSingleton data()[140] 3.097s passed
lenOfSeqConcat data()[141] 3.098s passed
lenOfSeqSub data()[142] 3.091s passed
lenOfSeqReverse data()[143] 3.090s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.089s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.095s passed
getOfSeqSingletonEQ data()[146] 3.110s passed
getOfSeqConcatEQ data()[147] 3.108s passed
getOfSeqSubEQ data()[148] 3.106s passed
getOfSeqReverseEQ data()[149] 3.102s passed
div_exists data()[14] 3.422s passed
lenOfSeqEmptyEQ data()[150] 3.261s passed
lenOfSeqSingletonEQ data()[151] 3.193s passed
lenOfSeqConcatEQ data()[152] 3.091s passed
lenOfSeqSubEQ data()[153] 3.107s passed
lenOfSeqReverseEQ data()[154] 3.093s passed
getOfSeqDefEQ data()[155] 3.096s passed
lenOfSeqDefEQ data()[156] 3.193s passed
seqConcatWithSeqEmpty1 data()[157] 3.102s passed
seqConcatWithSeqEmpty2 data()[158] 3.098s passed
seqReverseOfSeqEmpty data()[159] 3.108s passed
div_one data()[15] 3.155s passed
subSeqComplete data()[160] 3.095s passed
subSeqTailR data()[161] 3.146s passed
subSeqTailL data()[162] 3.103s passed
subSeqTailEQR data()[163] 3.155s passed
subSeqTailEQL data()[164] 3.098s passed
seqDef_split data()[165] 3.129s passed
seqDef_induction_upper data()[166] 3.112s passed
seqDef_induction_upper_concrete data()[167] 3.138s passed
seqDef_induction_lower data()[168] 3.108s passed
seqDef_induction_lower_concrete data()[169] 3.123s passed
jdiv_one data()[16] 3.127s passed
seqDef_split_in_three data()[170] 3.154s passed
seqDef_empty data()[171] 3.096s passed
seqDef_one_summand data()[172] 3.110s passed
seqDef_lower_equals_upper data()[173] 3.111s passed
seqDefOfSeq data()[174] 3.103s passed
seqSelfDefinitionEQ2 data()[175] 3.112s passed
indexOfSeqSingleton data()[176] 3.107s passed
indexOfSeqConcatFirst data()[177] 3.126s passed
indexOfSeqConcatSecond data()[178] 3.103s passed
indexOfSeqSub data()[179] 3.135s passed
div_zero data()[17] 3.178s passed
lenOfArray2seq data()[180] 3.112s passed
getAnyOfArray2seq data()[181] 3.114s passed
getOfArray2seq data()[182] 3.107s passed
getAnyOfNPermInv data()[183] 3.094s passed
seqNPermRange data()[184] 3.144s passed
seqPermTrans data()[185] 3.178s passed
seqPermRefl data()[186] 3.116s passed
seqPermSplit data()[187] 3.093s passed
seqNPermRight data()[188] 3.206s passed
seqPermFromSwap data()[189] 3.158s passed
divResZero1 data()[18] 3.133s passed
seqPermTransAlt0 data()[190] 3.105s passed
seqPermTransAlt1 data()[191] 3.107s passed
seqPermTransAlt2 data()[192] 3.096s passed
seqPermTransAlt3 data()[193] 3.116s passed
seqPermForall data()[194] 3.175s passed
seqPermExists data()[195] 3.181s passed
schiffl_lemma_2 data()[196] 22.363s passed
schiffl_thm_1 data()[197] 3.907s passed
eqSameSeq data()[198] 3.253s passed
divResZero2 data()[19] 3.174s passed
eqTermCut data()[1] 3.763s passed
divResOne1 data()[20] 3.163s passed
divResOne2 data()[21] 3.127s passed
div_cancel1 data()[22] 3.184s passed
div_cancel2 data()[23] 3.135s passed
divAddMultDenom data()[24] 3.194s passed
divMinus data()[25] 3.150s passed
divMinusDenom data()[26] 3.154s passed
divLeastDPos data()[27] 3.116s passed
divLeastDNeg data()[28] 3.137s passed
divGreatestDPos data()[29] 3.112s passed
equivAllRight data()[2] 3.406s passed
divGreatestDNeg data()[30] 3.130s passed
divIncreasingPos data()[31] 3.204s passed
divIncreasingNeg data()[32] 3.140s passed
jdiv_zero data()[33] 3.262s passed
jdivPulloutMinusNum data()[34] 3.269s passed
jdivPulloutMinusDenom data()[35] 3.299s passed
jdiv_uniquePosPos data()[36] 3.109s passed
jdiv_uniquePosNeg data()[37] 3.127s passed
jdiv_uniqueNegPos data()[38] 3.133s passed
jdiv_uniqueNegNeg data()[39] 3.128s passed
irrflConcrete1 data()[3] 3.313s passed
jdivMultDenom1 data()[40] 3.185s passed
jdivMultDenom2 data()[41] 3.170s passed
mod_geZero data()[42] 3.308s passed
mod_lessDenom data()[43] 3.242s passed
jmod_NumPos data()[44] 3.126s passed
jmod_NumNeg data()[45] 3.111s passed
jmod_geZero data()[46] 3.107s passed
jmodNumZero data()[47] 3.094s passed
jmod_pulloutminusNum data()[48] 3.180s passed
jmod_pulloutminusDenom data()[49] 3.096s passed
irrflConcrete2 data()[4] 3.249s passed
jmodUnique1 data()[50] 3.151s passed
jmodUnique2 data()[51] 3.182s passed
intDivRem data()[52] 3.146s passed
jmodjmod data()[53] 3.130s passed
jmodDivisible data()[54] 3.115s passed
jmodDivisibleRep data()[55] 3.135s passed
jdivAddMultDenom data()[56] 3.206s passed
jmodAltZero data()[57] 3.102s passed
jmodAddMultDenomZero data()[58] 3.084s passed
polyDiv_zero data()[59] 3.101s passed
cancel_gtPos data()[5] 3.266s passed
polyMod_ltdivDenom data()[60] 3.098s passed
bsum_empty data()[61] 3.074s passed
bsum_induction_upper data()[62] 3.097s passed
bsum_induction_lower data()[63] 3.089s passed
bsum_num_of_bounds data()[64] 3.130s passed
bsum_num_of_bounds2 data()[65] 3.088s passed
bsum_induction_upper2 data()[66] 3.098s passed
bsum_induction_upper_concrete data()[67] 3.085s passed
bsum_induction_upper_concrete_2 data()[68] 3.105s passed
bsum_induction_upper2_concrete data()[69] 3.078s passed
cancel_gtNeg data()[6] 3.262s passed
bsum_induction_lower_concrete data()[70] 3.090s passed
bsum_induction_lower2 data()[71] 3.096s passed
bsum_induction_lower2_concrete data()[72] 3.130s passed
bsum_positive data()[73] 3.122s passed
bsum_upper_bound data()[74] 3.109s passed
bsum_lower_bound data()[75] 3.122s passed
bsum_positive_lower_bound_element data()[76] 3.110s passed
bsum_sub_same_index data()[77] 3.110s passed
bsum_less_same_index data()[78] 3.148s passed
bsum_equal_except_one_index data()[79] 3.158s passed
moduloIntIsInInt data()[7] 3.263s passed
bsum_num_of_is_max data()[80] 3.107s passed
bsum_num_of_is_max2 data()[81] 3.099s passed
bsum_num_of_is_max3 data()[82] 3.110s passed
bsum_num_of_is_max4 data()[83] 3.108s passed
bsum_num_of_lt_max data()[84] 3.111s passed
bsum_num_of_lt_max2 data()[85] 3.088s passed
bsum_num_of_lt_max3 data()[86] 3.141s passed
bsum_num_of_lt_max4 data()[87] 3.228s passed
bsum_num_of_gt0 data()[88] 3.254s passed
bsum_num_of_gt0_alt data()[89] 3.256s passed
moduloLongIsInLong data()[8] 3.178s passed
bsum_add_concrete data()[90] 3.223s passed
bprod_all_positive data()[91] 3.206s passed
bprod_split data()[92] 3.082s passed
powConcrete0 data()[93] 3.146s passed
powConcrete1 data()[94] 3.071s passed
powSplitFactor data()[95] 3.106s passed
powAdd data()[96] 3.082s passed
powMono data()[97] 3.102s passed
powMonoConcrete data()[98] 3.076s passed
powMonoConcreteRight data()[99] 3.095s passed
moduloShortIsInShort data()[9] 3.159s passed

Standard output

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

1486       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1517       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1518       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1519       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2760       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7526       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.94s 
7591       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7622       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.7ns 
7633       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7634       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.5ns 
7638       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
10436      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11389      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.58ms 
11397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns 
11398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
13954      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
14803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
14804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17288      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
17288      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18114      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
18116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.1ns 
18117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
20545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21363      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
21365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
21366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23757      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
23757      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24629      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.14ms 
24630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
24636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27059      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
27060      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27891      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.55ms 
27894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27894      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.8ns 
27895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
30337      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31155      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.3ns 
31157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.3ns 
31159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
33549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570ns 
34336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.2ns 
34337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
36733      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37493      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.7ns 
37496      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37496      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.9ns 
37498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
39873      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40655      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600ns 
40659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 569.1ns 
40660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43053      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
43053      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43830      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.6ns 
43832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43832      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns 
43833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
46200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47032      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.98ms 
47034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
47035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
49425      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50221      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.17ms 
50223      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50223      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
50224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
52671      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.4ms 
53645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 
53646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
56027      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56798      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
56799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
56800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
59165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
59928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.4ns 
59930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62297      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
62297      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63104      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.26ms 
63106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.6ns 
63108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
65477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66237      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
66239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.3ns 
66240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
68628      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69410      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.38ms 
69413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 837.9ns 
69420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
71792      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.02ms 
72576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.5ns 
72578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
74927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75701      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
75703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.8ns 
75705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
78066      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78885      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
78887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 
78888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
81257      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82021      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
82022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
82023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
84411      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85214      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.16ms 
85216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300ns 
85218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
87559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.48ms 
88366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88367      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.7ns 
88368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
90729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91519      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.73ms 
91520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
91521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
93879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
94636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 920.5ns 
94638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
97001      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97772      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
97773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
97774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
100132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
100905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
100906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
103246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
104014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.6ns 
104016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
106451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
107218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
107219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
109591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
110358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
110359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
112831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
113623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
113624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
116101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
116892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
116893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
119382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.81ms 
120192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.3ns 
120194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
122547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
123285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
123299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
123301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
123301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.2ns 
123302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
125655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
126428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
126429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
128805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
129561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
129562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
131918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
132689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
132690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
135042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.06ms 
135876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
135877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
138261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
139042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
139044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885.1ns 
139046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
139046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
139046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
141532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
142348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
142352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
142353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
142353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
142354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
144819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
145587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
145594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
145595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
145595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
145596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
147943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
148721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
148722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
151055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
151818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
151832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.04ms 
151833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
151833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
151834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
154176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
154940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
154941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
157283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
158034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.6ns 
158035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
160431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
161214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
161214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
163569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
164306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
164309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
164310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
164310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
164311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
166654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
167409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
167460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.29ms 
167461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
167461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
167462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
169811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
170566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
170641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.16ms 
170646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
170646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.3ns 
170647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
173025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
173786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
173789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.5ns 
173791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
173791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.4ns 
173792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
176135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
176888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
176918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.05ms 
176921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
176925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.08ms 
176926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
179260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.43ms 
180036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
180037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
182409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
183164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
183169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
183171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
183171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
183172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
185541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
186282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
186375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.23ms 
186377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
186377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
186377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
188716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
189470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
189477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
189478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
189479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
189479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
191820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
192556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
192561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
192563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
192563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
192563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
194898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
195650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
195663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
195664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
195664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
195665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
198000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
198750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
198760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
198761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
198761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
198762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
201081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
201836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
201836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
204175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
204928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
204931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
204932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
204932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
204933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
207255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
208007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
208020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
208021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
208021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
208022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
210382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
211139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
211151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
211152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
211152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
211153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
213475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
214228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
214239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
214240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
214240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
214241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
216579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
217333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
217336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
217339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
217339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
217340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
219683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
220419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
220421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
220422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
220423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
220423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
222770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
223522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
223527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
223528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
223528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
223528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
225869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
226602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
226604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.8ns 
226605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
226606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
226606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
228942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
229693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
229694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 406ns 
229696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
229696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
229696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
232035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
232788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
232791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
232792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
232792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
232793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
235163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
235918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
235920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.4ns 
235921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
235921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
235922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
238259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
239011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
239042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.89ms 
239044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
239044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.6ns 
239045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
241371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
242123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
242151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.46ms 
242152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
242152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
242153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
244497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
245250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
245273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
245274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
245274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
245275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
247599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
248351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
248384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.42ms 
248385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
248385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
248386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
250721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
251473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
251493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.25ms 
251494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
251494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
251495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
253844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
254599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
254641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.52ms 
254643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
254643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
254643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
257026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
257778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
257799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.45ms 
257800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
257800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
257801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
260141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
260893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
260907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
260908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
260908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
260909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
263234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
263989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
264005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.87ms 
264006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
264006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
264007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
266351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
267103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
267116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
267117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
267118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.6ns 
267118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
269446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
270206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
270223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.35ms 
270224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
270224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
270225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
272565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
273318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
273334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms 
273335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
273335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
273336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
275653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
276405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
276422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
276423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
276423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
276424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
278767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
279547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
279563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
279564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
279564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
279565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
282019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
282776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
282791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
282792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
282793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
282793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
285246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
286022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
286045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
286046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
286046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
286047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
288509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
289286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
289301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms 
289302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
289302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
289303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
291742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
292518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
292524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
292525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
292525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
292526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
294967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
295718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
295730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
295731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
295731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
295732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
298052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
298810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
298813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
298814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
298814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
298815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
301205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
301956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
301958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.6ns 
301959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
301959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
301960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
304274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
305027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
305030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.6ns 
305031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
305031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.5ns 
305032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
307376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
308130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
308136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
308137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
308137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
308138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
310472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
311212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
311217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
311219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
311219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns 
311220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
313552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
314310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
314320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
314321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
314321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
314321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
316658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
317392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
317396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
317397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
317397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
317398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
319735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
320488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
320490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.1ns 
320491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
320491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
320492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
322831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
323583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
323588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
323589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
323589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
323590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
325910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
326667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
326669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.3ns 
326670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
326670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
326671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
329007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
329764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
329766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.3ns 
329767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
329767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
329768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
332102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
332857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
332858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.4ns 
332860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
332860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
332860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
335179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
335931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
335934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
335935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
335935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
335935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
338264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
339018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
339028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
339029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
339029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.7ns 
339030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
341365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
342100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
342103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
342104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
342104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
342104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
344443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
345195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
345200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
345201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
345201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
345202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
347534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
348288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
348291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
348292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
348293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
348293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
350630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
351381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
351392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.58ms 
351393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
351393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
351394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
353711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
354465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
354468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
354469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
354469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
354469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
356810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
357564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
357566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.6ns 
357567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
357567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
357568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
359901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
360653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
360656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
360657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
360657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
360658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
362996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
363732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
363744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
363745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
363745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
363746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
366080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
366831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
366835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 371.6ns 
366837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
366837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
366837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
369162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
369912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
369937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.96ms 
369939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
369939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
369940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
372274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
373026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
373029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
373030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
373030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
373030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
375368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
376122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
376136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
376138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
376138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns 
376139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
378459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
379211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
379224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
379225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
379225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
379226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
381559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
382314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
382331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
382332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
382332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
382333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
384665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
385418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
385420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 426.6ns 
385421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
385421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
385422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
387758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
388511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
388515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
388516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
388516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
388517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
390845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
391603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
391606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
391607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
391607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
391608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
393942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
394697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
394699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.1ns 
394700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
394700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
394701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
397035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
397790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
397792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.1ns 
397793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
397793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
397794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
400129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
400868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
400870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 896.9ns 
400871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
400871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
400872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
403199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
403955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
403957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.5ns 
403959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
403959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
403959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
406289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
407044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
407052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
407053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
407053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
407054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
409383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
410142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
410148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
410149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
410149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
410150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
412480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
413237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
413243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
413244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
413244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
413245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
415574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
416335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
416342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
416343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
416343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
416343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
418673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
419437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
419441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
419442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
419442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
419442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
421778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
422542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
422545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
422546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
422546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
422547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
424882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
425645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
425647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.9ns 
425648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
425648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
425649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
427977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
428743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
428745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.6ns 
428746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
428746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
428747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
431076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
431839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
431841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.1ns 
431843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
431843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
431843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
434176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
434939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
434947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
434948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
434948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
434949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
437277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
438038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
438041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
438042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
438042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
438043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
440371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
441131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
441135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
441136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
441137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
441137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
443490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
444251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
444253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 631.8ns 
444254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
444255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
444255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
446587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
447348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
447350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 472.5ns 
447351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
447351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
447351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
449681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
450445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
450448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
450449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
450449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
450449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
452778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
453537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
453539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.2ns 
453540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
453540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
453540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
455866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
456626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
456629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.3ns 
456630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
456630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
456630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
458955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
459716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
459718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.4ns 
459719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
459719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
459719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
462048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
462809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
462812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
462813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
462813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
462814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
465158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
465920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
465922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.2ns 
465923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
465923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
465924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
468262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
469022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
469030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
469031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
469031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
469032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
471358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
472135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
472137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392ns 
472138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
472138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
472139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
474468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
475234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
475239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
475240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
475240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.2ns 
475240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
477711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
478497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
478499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 807.7ns 
478500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
478500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
478501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
480930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
481690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
481692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.5ns 
481693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
481693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
481694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
484020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
484780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
484783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
484785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
484785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.4ns 
484785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
487129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
487888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
487891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.5ns 
487892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
487893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.3ns 
487893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
490220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
490981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
490984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
490985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
490985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
490985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
493316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
494077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
494080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
494082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
494082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.3ns 
494083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
496509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
497270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
497274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
497275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
497275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.2ns 
497276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
499602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
500369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
500375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
500376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
500376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
500377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
502704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
503466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
503473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
503474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
503474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
503475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
505818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
506577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
506582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
506583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
506583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
506584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
508910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
509671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
509677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
509678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
509678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
509678     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 2.35s 
512032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
512813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
512823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
512824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
512824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
512825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
515157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
515916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
515926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
515927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
515927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
515927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
518311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
519072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
519081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.58ms 
519082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
519082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
519082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
521411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
522172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
522178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
522179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
522179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
522180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
524527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
525288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
525307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
525308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
525308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
525309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
527638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
528399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
528419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms 
528420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
528420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
528421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
530774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
531537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
531557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.68ms 
531558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
531558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
531559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
533887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
534648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
534665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
534666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
534666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
534667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
537010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
537771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
537789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.45ms 
537790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
537790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
537790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
540138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
540899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
540943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms 
540944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
540944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
540945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
543275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
544035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
544039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
544040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
544040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
544040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
546383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
547144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
547149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
547150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
547150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.5ns 
547150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
549496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
550257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
550260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
550261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
550261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
550262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
552588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
553350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
553362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
553363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
553363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
553364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
555707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
556469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
556475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
556476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
556476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
556477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
558819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
559579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
559582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
559583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
559583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
559584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
561921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
562698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
562708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
562709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
562709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
562709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
565036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
565796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
565810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
565811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
565812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.6ns 
565812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
568170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
568933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
568945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
568946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
568946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
568947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
571295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
572056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
572058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.6ns 
572059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
572059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
572060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
574406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
575168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
575171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
575172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
575172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
575173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
577496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
578274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
578279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
578280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
578280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.2ns 
578280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
580607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
581369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
581373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
581374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
581374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
581375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
583717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
584478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
584517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.68ms 
584518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
584518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
584519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
586889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
587677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
587694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.22ms 
587695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
587696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
587696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
590040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
590800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
590810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
590811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
590811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
590812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
593141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
593902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
593904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 217.2ns 
593905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
593905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43ns 
593906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
596255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
597018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
597109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.99ms 
597111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
597112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.9ns 
597112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
599452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
600213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
600267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.16ms 
600269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
600269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
600269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
602607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
603371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
603373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.3ns 
603374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
603374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
603374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
605717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
606478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
606479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.2ns 
606480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
606480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
606481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
608807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
609573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
609575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 179.2ns 
609576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
609576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.5ns 
609577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
611925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
612690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
612691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.6ns 
612692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
612692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
612693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
615025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
615787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
615866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.23ms 
615868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
615868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.6ns 
615869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
618246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
619009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
619047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.36ms 
619048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
619049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
619050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
621396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
622196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
622198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
622221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
622256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
622271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
622275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
622282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
622284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
622285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
622286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
622289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
622291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
622293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
622294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
622517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
622519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
622521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
622522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
622523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
622666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
622667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
622670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
622672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
622673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
622674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
622847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
622849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
622850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
622851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
622852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
622855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
622987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
622989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
622990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
622991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
622992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
622993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
623001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
623002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
623003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
623004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
623005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
623006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
623013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
623014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
623014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
623015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
623016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
623017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
623168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
623169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
623169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
623302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
623304     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)'' 
623306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
623306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
623307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
623308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
623309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
623309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
623313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
623314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
623315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
623316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
623316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
623429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
623433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
623434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
623435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
623436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
623436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
623437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
623567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
623569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
623569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
623571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
623571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
623572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
623573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
623574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
623670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
623672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
623769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
623774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
623779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
623780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
623781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
623782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
623782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
623783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
623783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
623790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
623799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
623804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
623907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
623909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
623909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
623910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
623911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
623912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
623912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
623913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
623969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
623975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
624085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
624087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
624089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
624090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
624091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
624092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
624272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
624276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
624278     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)'' 
624279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
624280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
624281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
624282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
624282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
624292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
624293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
624294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
624294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
624391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
624392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
624393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
624394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
624394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
624395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
624499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
624500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
624501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
624502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
624503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
624503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
624504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
624505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
624588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
624589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
624667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
624668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
624669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
624673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
624677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
624682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
624830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
624831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
624832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
624833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
624842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
624923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
628598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
628599     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)'' 
628604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
628610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
628611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
628611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
628612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
628620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
628621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
628622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
628623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
628623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
628715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
628719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
628720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
628721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
628721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
628722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
628723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
628817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
628818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
628819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
628820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
628821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
628821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
628822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
628823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
628898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
628899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
628972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
628976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
628981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
628981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
628982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
628983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
628993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
629072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
629073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
629074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
629075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
629148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
629157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
629158     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)'' 
629160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
629160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
629161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
629162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
629162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
629173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
629174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
629175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
629175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
629176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
629262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
629264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
629264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
629265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
629265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
629355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
629360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
629360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
629361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
629361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
629362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
629362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
629459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
629460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
629461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
629462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
629462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
629463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
629463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
629464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
629465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
629466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
629467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
629467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
629468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
629468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
629469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
629556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
629557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
629564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
629643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
629723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
629724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
629725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
629725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
629726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
629726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
629727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
629727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
629728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
629813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
629819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
629908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
629909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
629909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
629910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
629911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
629911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
629911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
629912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
629917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
629918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
629997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
630002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
630007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
630142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
630143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
630144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
630145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
630145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
630145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
630146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
630146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
630200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
630201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
630201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
630202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
630203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
630208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
630213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
630327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
630414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
630415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
630415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
630416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
630579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
630667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
630668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
633739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
633744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
633745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
633745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
633746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
633856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
633858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
633858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
633859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
633859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
633964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
636937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
640153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
640157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
640158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
640158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
640159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
640269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
640270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
640271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
640272     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)' ...' 
640273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
641412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
641412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
641412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
643825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
644604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
644605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
644606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
644614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
644624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
644626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
644627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
644628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
644632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
644633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
644637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
644639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
644639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
644649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
644650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
644651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
644697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
644698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
644698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
644699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
644699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
644761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
644761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
644762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
644763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
644763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
644766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
644767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
644767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
644768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
644769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
644769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
644851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
644852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
644853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
644854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
644854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
644855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
644944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
644945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
644945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
644946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
644947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
644947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
644948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
644948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
644949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
644950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
644950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
644950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
644951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
644951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
644952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
644952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
644953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
644954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
644954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
644957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
644996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
644997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
645058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
645059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
645061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
645062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
645062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
645063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
645119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
645122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
645123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
645124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
645125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
645126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
645126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
645179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
645182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
645185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
645251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
645319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
645319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.9ns 
645320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
647752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
648555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
648570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms