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

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

tests
0

failures
0

ignored
10m54.14s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.173s passed
powPositiveConcrete data()[101] 3.171s passed
powGeq1Concrete data()[102] 3.160s passed
pow2InIntLower data()[103] 3.169s passed
pow2InIntUpper data()[104] 3.156s passed
logSelfConcrete data()[105] 3.155s passed
log1Concrete data()[106] 3.150s passed
logProduct data()[107] 3.150s passed
logTimesBaseConcrete data()[108] 3.145s passed
logProdIdentity data()[109] 3.158s passed
moduloByteIsInByte data()[10] 3.247s passed
logProdIdentityConcrete data()[110] 3.168s passed
logPowIdentity data()[111] 3.185s passed
logPowIdentityConcrete data()[112] 3.153s passed
logPositive data()[113] 3.166s passed
logPositiveConcrete data()[114] 3.156s passed
logMono data()[115] 3.173s passed
logMonoConcrete data()[116] 3.138s passed
powLogLess data()[117] 3.159s passed
powLogMore2 data()[118] 3.157s passed
logLessThanPow data()[119] 3.160s passed
moduloCharIsInChar data()[11] 3.225s passed
logLessThanPowConcrete data()[120] 3.184s passed
logSqueeze data()[121] 3.170s passed
ifthenelse_equals data()[122] 3.163s passed
ifthenelse_equals_1 data()[123] 3.161s passed
ifthenelse_equals_2 data()[124] 3.153s passed
disjointWithSingleton1 data()[125] 3.163s passed
disjointWithSingleton2 data()[126] 3.152s passed
disjointArrayRanges data()[127] 3.189s passed
disjointArrayRangeAllFields1 data()[128] 3.170s passed
disjointArrayRangeAllFields2 data()[129] 3.173s passed
div_unique1 data()[12] 3.314s passed
seqSelfDefinition data()[130] 3.173s passed
seqOutsideValue data()[131] 3.152s passed
castedGetAny data()[132] 3.181s passed
seqGetAlphaCast data()[133] 3.163s passed
getOfSeqSingleton data()[134] 3.151s passed
getOfSeqSingletonConcrete data()[135] 3.146s passed
getOfSeqConcat data()[136] 3.146s passed
getOfSeqSub data()[137] 3.167s passed
getOfSeqReverse data()[138] 3.154s passed
lenOfSeqEmpty data()[139] 3.162s passed
div_unique2 data()[13] 3.296s passed
lenOfSeqSingleton data()[140] 3.185s passed
lenOfSeqConcat data()[141] 3.173s passed
lenOfSeqSub data()[142] 3.161s passed
lenOfSeqReverse data()[143] 3.177s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.160s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.160s passed
getOfSeqSingletonEQ data()[146] 3.188s passed
getOfSeqConcatEQ data()[147] 3.183s passed
getOfSeqSubEQ data()[148] 3.163s passed
getOfSeqReverseEQ data()[149] 3.184s passed
div_exists data()[14] 3.511s passed
lenOfSeqEmptyEQ data()[150] 3.152s passed
lenOfSeqSingletonEQ data()[151] 3.161s passed
lenOfSeqConcatEQ data()[152] 3.183s passed
lenOfSeqSubEQ data()[153] 3.147s passed
lenOfSeqReverseEQ data()[154] 3.192s passed
getOfSeqDefEQ data()[155] 3.157s passed
lenOfSeqDefEQ data()[156] 3.175s passed
seqConcatWithSeqEmpty1 data()[157] 3.174s passed
seqConcatWithSeqEmpty2 data()[158] 3.217s passed
seqReverseOfSeqEmpty data()[159] 3.190s passed
div_one data()[15] 3.229s passed
subSeqComplete data()[160] 3.210s passed
subSeqTailR data()[161] 3.198s passed
subSeqTailL data()[162] 3.208s passed
subSeqTailEQR data()[163] 3.182s passed
subSeqTailEQL data()[164] 3.195s passed
seqDef_split data()[165] 3.184s passed
seqDef_induction_upper data()[166] 3.223s passed
seqDef_induction_upper_concrete data()[167] 3.199s passed
seqDef_induction_lower data()[168] 3.209s passed
seqDef_induction_lower_concrete data()[169] 3.228s passed
jdiv_one data()[16] 3.248s passed
seqDef_split_in_three data()[170] 3.275s passed
seqDef_empty data()[171] 3.191s passed
seqDef_one_summand data()[172] 3.175s passed
seqDef_lower_equals_upper data()[173] 3.154s passed
seqDefOfSeq data()[174] 3.179s passed
seqSelfDefinitionEQ2 data()[175] 3.170s passed
indexOfSeqSingleton data()[176] 3.153s passed
indexOfSeqConcatFirst data()[177] 3.205s passed
indexOfSeqConcatSecond data()[178] 3.191s passed
indexOfSeqSub data()[179] 3.177s passed
div_zero data()[17] 3.230s passed
lenOfArray2seq data()[180] 3.185s passed
getAnyOfArray2seq data()[181] 3.178s passed
getOfArray2seq data()[182] 3.181s passed
getAnyOfNPermInv data()[183] 3.165s passed
seqNPermRange data()[184] 3.239s passed
seqPermTrans data()[185] 3.211s passed
seqPermRefl data()[186] 3.193s passed
seqPermSplit data()[187] 3.182s passed
seqNPermRight data()[188] 3.397s passed
seqPermFromSwap data()[189] 3.237s passed
divResZero1 data()[18] 3.204s passed
seqPermTransAlt0 data()[190] 3.185s passed
seqPermTransAlt1 data()[191] 3.175s passed
seqPermTransAlt2 data()[192] 3.164s passed
seqPermTransAlt3 data()[193] 3.164s passed
seqPermForall data()[194] 3.278s passed
seqPermExists data()[195] 3.285s passed
schiffl_lemma_2 data()[196] 22.582s passed
schiffl_thm_1 data()[197] 4.018s passed
eqSameSeq data()[198] 3.232s passed
divResZero2 data()[19] 3.229s passed
eqTermCut data()[1] 3.847s passed
divResOne1 data()[20] 3.275s passed
divResOne2 data()[21] 3.233s passed
div_cancel1 data()[22] 3.241s passed
div_cancel2 data()[23] 3.207s passed
divAddMultDenom data()[24] 3.228s passed
divMinus data()[25] 3.269s passed
divMinusDenom data()[26] 3.278s passed
divLeastDPos data()[27] 3.194s passed
divLeastDNeg data()[28] 3.206s passed
divGreatestDPos data()[29] 3.200s passed
equivAllRight data()[2] 3.550s passed
divGreatestDNeg data()[30] 3.183s passed
divIncreasingPos data()[31] 3.192s passed
divIncreasingNeg data()[32] 3.212s passed
jdiv_zero data()[33] 3.204s passed
jdivPulloutMinusNum data()[34] 3.221s passed
jdivPulloutMinusDenom data()[35] 3.281s passed
jdiv_uniquePosPos data()[36] 3.246s passed
jdiv_uniquePosNeg data()[37] 3.189s passed
jdiv_uniqueNegPos data()[38] 3.196s passed
jdiv_uniqueNegNeg data()[39] 3.184s passed
irrflConcrete1 data()[3] 3.477s passed
jdivMultDenom1 data()[40] 3.202s passed
jdivMultDenom2 data()[41] 3.161s passed
mod_geZero data()[42] 3.194s passed
mod_lessDenom data()[43] 3.201s passed
jmod_NumPos data()[44] 3.186s passed
jmod_NumNeg data()[45] 3.203s passed
jmod_geZero data()[46] 3.179s passed
jmodNumZero data()[47] 3.172s passed
jmod_pulloutminusNum data()[48] 3.176s passed
jmod_pulloutminusDenom data()[49] 3.161s passed
irrflConcrete2 data()[4] 3.443s passed
jmodUnique1 data()[50] 3.231s passed
jmodUnique2 data()[51] 3.253s passed
intDivRem data()[52] 3.193s passed
jmodjmod data()[53] 3.206s passed
jmodDivisible data()[54] 3.201s passed
jmodDivisibleRep data()[55] 3.179s passed
jdivAddMultDenom data()[56] 3.301s passed
jmodAltZero data()[57] 3.187s passed
jmodAddMultDenomZero data()[58] 3.157s passed
polyDiv_zero data()[59] 3.176s passed
cancel_gtPos data()[5] 3.375s passed
polyMod_ltdivDenom data()[60] 3.165s passed
bsum_empty data()[61] 3.144s passed
bsum_induction_upper data()[62] 3.159s passed
bsum_induction_lower data()[63] 3.191s passed
bsum_num_of_bounds data()[64] 3.218s passed
bsum_num_of_bounds2 data()[65] 3.182s passed
bsum_induction_upper2 data()[66] 3.163s passed
bsum_induction_upper_concrete data()[67] 3.172s passed
bsum_induction_upper_concrete_2 data()[68] 3.171s passed
bsum_induction_upper2_concrete data()[69] 3.160s passed
cancel_gtNeg data()[6] 3.329s passed
bsum_induction_lower_concrete data()[70] 3.173s passed
bsum_induction_lower2 data()[71] 3.166s passed
bsum_induction_lower2_concrete data()[72] 3.199s passed
bsum_positive data()[73] 3.223s passed
bsum_upper_bound data()[74] 3.225s passed
bsum_lower_bound data()[75] 3.191s passed
bsum_positive_lower_bound_element data()[76] 3.227s passed
bsum_sub_same_index data()[77] 3.183s passed
bsum_less_same_index data()[78] 3.190s passed
bsum_equal_except_one_index data()[79] 3.178s passed
moduloIntIsInInt data()[7] 3.287s passed
bsum_num_of_is_max data()[80] 3.174s passed
bsum_num_of_is_max2 data()[81] 3.192s passed
bsum_num_of_is_max3 data()[82] 3.189s passed
bsum_num_of_is_max4 data()[83] 3.207s passed
bsum_num_of_lt_max data()[84] 3.180s passed
bsum_num_of_lt_max2 data()[85] 3.176s passed
bsum_num_of_lt_max3 data()[86] 3.178s passed
bsum_num_of_lt_max4 data()[87] 3.175s passed
bsum_num_of_gt0 data()[88] 3.169s passed
bsum_num_of_gt0_alt data()[89] 3.173s passed
moduloLongIsInLong data()[8] 3.295s passed
bsum_add_concrete data()[90] 3.193s passed
bprod_all_positive data()[91] 3.164s passed
bprod_split data()[92] 3.152s passed
powConcrete0 data()[93] 3.149s passed
powConcrete1 data()[94] 3.155s passed
powSplitFactor data()[95] 3.161s passed
powAdd data()[96] 3.150s passed
powMono data()[97] 3.151s passed
powMonoConcrete data()[98] 3.139s passed
powMonoConcreteRight data()[99] 3.138s passed
moduloShortIsInShort data()[9] 3.290s passed

Standard output

280        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
302        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.01ms 
508        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521        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)

1418       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1420       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1422       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1423       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3074       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8316       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.81s 
8380       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8414       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36ns 
8428       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8429       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 664.61ns 
8434       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
11230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12266      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.31ms 
12280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.31ns 
12282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
14897      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
15830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.3ns 
15833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
18487      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19305      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
19310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.41ns 
19312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
21920      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22751      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
22754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.11ns 
22756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25277      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
25278      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26125      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.42ms 
26129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.71ns 
26131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28633      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
28633      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29456      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms 
29458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
29459      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
31905      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32743      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.31ns 
32746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.41ns 
32747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
35230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.61ns 
36041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 
36042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38491      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
38491      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39326      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
39332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.91ns 
39334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
41777      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42578      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.41ns 
42579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
42582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
45027      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.71ns 
45805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.91ns 
45806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
48287      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49110      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.56ms 
49124      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 468.81ns 
49126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
51576      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52416      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.66ms 
52420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 742.81ns 
52422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
54868      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 258.76ms 
55930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.2ns 
55931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
58357      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59157      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
59159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59160      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.7ns 
59161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61603      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
61604      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62405      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
62407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62408      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.7ns 
62409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
64811      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65635      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.41ms 
65637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
65638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68039      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
68040      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68839      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
68841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.5ns 
68842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
71246      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72068      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
72070      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72071      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 658.91ns 
72072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74512      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
74512      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
75345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.6ns 
75346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77790      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
77791      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
78578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.2ns 
78579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
81034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81818      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
81819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.5ns 
81820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
84233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85024      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
85026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.21ns 
85028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87432      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
87433      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88252      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.65ms 
88254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.01ns 
88256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
90664      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91520      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.8ms 
91523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.11ns 
91525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
93949      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.84ms 
94801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.9ns 
94802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
97204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97993      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
97995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97995      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
97996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
100394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
101186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
101199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
101201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
101201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
101202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
103611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
104401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
104402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
106811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
107584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
107585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
110004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
110776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.41ns 
110777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
113213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
113988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
113989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
116401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
117187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
117190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
117192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
117192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
117193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
119607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
120399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
120411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
120413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
120414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.61ns 
120415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
122812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
123603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
123692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.74ms 
123696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
123696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.11ns 
123698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
126086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
126909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
126939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.66ms 
126949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
126949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.11ns 
126950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
129336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
130117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
130136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
130138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
130138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
130139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
132526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
133312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
133332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.93ms 
133334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
133335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.61ns 
133336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
135718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
136516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
136517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
136517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
136518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
138920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
139675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
139718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.24ms 
139720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
139721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.7ns 
139721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
142121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
142877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
142880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.52ns 
142881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
142881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
142882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
145312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
146069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
146074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
146075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
146075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
146076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
148482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
149266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
149274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
149275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
149276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
149276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
151660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
152460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.95ms 
152463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
152464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 832.82ns 
152465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
154862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
155644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
155664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.34ms 
155665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
155665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 
155666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
158059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
158835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
158843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
158845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
158845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
158846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
161220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
162012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
162016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
162017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
162017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns 
162018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
164409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
165186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
165191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
165192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
165193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
165193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
167566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
168346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
168352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
168355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
168356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.61ns 
168358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
170761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
171513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
171584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.19ms 
171586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
171586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
171587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
174005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
174758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
174837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.48ms 
174839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
174839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
174840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
177240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
178026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
178030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
178032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
178032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.61ns 
178033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
180410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
181187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
181232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.65ms 
181237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
181238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
181238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
183631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
184408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
184438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.97ms 
184439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
184439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
184440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
186833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
187614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
187617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
187618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
187618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
187619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
189998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
190776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
190917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.01ms 
190919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
190919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
190920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
193314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
194093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
194104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
194105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
194105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
194106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
196474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
197253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
197261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
197262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
197262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
197263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
199670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
200421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
200437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
200439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
200439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
200439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
202837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
203588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
203601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
203604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
203604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.11ns 
203605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
205991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
206743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
206746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
206748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
206748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
206748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
209125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
209900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
209905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
209906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
209906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
209907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
212291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
213073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
213096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ms 
213098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
213098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
213099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
215511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
216296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
216313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
216316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
216316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.31ns 
216318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
218703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
219481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
219497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
219498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
219498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
219499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
221873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
222656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
222660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
222661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
222661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
222662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
225047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
225828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
225832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
225834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
225834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
225835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
228218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
228997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
229003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
229004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
229004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
229005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
231405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
232161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
232164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
232165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
232165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
232166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
234581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
235334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
235336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.21ns 
235338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
235338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
235338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
237744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
238499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
238503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
238504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
238504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.5ns 
238505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
240920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
241699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
241702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
241703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
241703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
241704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
244088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
244863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
244924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.17ms 
244926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
244926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
244927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
247328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
248107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
248150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.89ms 
248151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
248151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
248152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
250532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
251306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
251341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.34ms 
251342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
251342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
251343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
253744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
254519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
254567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.05ms 
254568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
254569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
254569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
256945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
257720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
257750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.43ms 
257752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
257752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
257753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
260119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
260892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
260941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.65ms 
260942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
260942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
260943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
263341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
264118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
264119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
264119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
264120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
266522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
267273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
267292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.24ms 
267294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
267294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
267295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
269678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
270458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
270484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
270486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
270486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
270487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
272877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
273653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
273673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ms 
273674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
273675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
273675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
276077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
276853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
276880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.1ms 
276882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
276882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
276882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
279257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
280035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
280060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.89ms 
280061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
280061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
280062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
282430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
283237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.09ms 
283238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
283238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
283239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
285611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
286390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
286415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.12ms 
286416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
286416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
286417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
288788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
289568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
289589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
289590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
289590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
289591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
291983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
292734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
292759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.95ms 
292760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
292760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
292761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
295155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
295906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
295931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms 
295932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
295932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
295933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
298339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
299116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
299124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
299125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
299125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
299126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
301497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
302288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
302290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
302290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
302290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
304660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
305436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
305440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
305441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
305441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
305442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
307812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
308587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
308589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.51ns 
308591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
308591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
308591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
310958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
311742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
311745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.51ns 
311746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
311746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
311747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
314118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
314894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
314905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
314907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
314907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
314908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
317271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
318049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
318055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
318056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
318056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
318057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
320419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
321206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.72ms 
321207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
321208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
321208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
323589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
324342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
324345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
324347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
324347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
324347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
326731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
327481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
327483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.31ns 
327485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
327485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
327485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
329868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
330650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
330657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
330658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
330658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
330659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
333046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
333825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
333828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.61ns 
333829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
333829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
333830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
336205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
336985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
336987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.01ns 
336988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
336988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
336989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
339372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
340153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
340156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.81ns 
340158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
340158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.1ns 
340159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
342530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
343308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
343312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
343313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
343313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
343314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
345680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
346458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
346467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
346469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
346470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.1ns 
346470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
348832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
349614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
349618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
349619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
349619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
349620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
351983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
352760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
352767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
352768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
352769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
352769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
355156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
355909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
355913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
355914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
355914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
355915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
358301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
359055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
359071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
359072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
359072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
359073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
361481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
362234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
362238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
362239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
362239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
362240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
364644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
365420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
365423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
365424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
365424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
365425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
367797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
368572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
368576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
368578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
368578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
368578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
370946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
371724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
371742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
371744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
371744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.41ns 
371745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
374118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
374894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
374898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.11ns 
374900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
374900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
374901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
377262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
378033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
378071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.48ms 
378073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
378073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
378073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
380432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
381206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
381209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
381211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
381211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
381211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
383573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
384346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
384368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.14ms 
384370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
384371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.6ns 
384371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
386754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
387505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
387525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.51ms 
387526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
387526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
387527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
389908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
390662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
390686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.29ms 
390687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
390687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
390688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
393087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
393867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
393870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.41ns 
393871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
393871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
393872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
396254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
397034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
397040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
397041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
397041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
397042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
399419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
400199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
400202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
400203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
400204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
400204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
402580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
403361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
403363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.22ns 
403365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
403365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
403365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
405733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
406513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
406516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
406517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
406517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
406518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
408895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
409676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
409680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
409681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
409681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
409682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
412069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
412828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
412831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
412832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
412832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
412833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
415227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
416010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
416021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
416022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
416023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.8ns 
416023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
418393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
419177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
419191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
419192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
419192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
419193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
421570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
422352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
422363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
422365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
422365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
422365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
424737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
425523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
425536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.94ms 
425538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
425538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
425538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
427919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
428684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
428688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
428689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
428690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
428690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
431074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
431863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
431869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
431870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
431870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
431871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
434242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
435030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
435032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 768.11ns 
435033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
435033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
435034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
437391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
438180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
438183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
438184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
438184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
438185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
440541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
441327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
441330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.72ns 
441331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
441331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
441331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
443703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
444464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
444475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
444476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
444476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
444477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
446849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
447639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
447643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
447644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
447644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
447645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
450003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
450790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
450796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
450798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
450798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
450798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
453191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
453956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
453958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.62ns 
453959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
453959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
453960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
456352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
457141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
457143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.61ns 
457144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
457144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
457145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
459523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
460312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
460316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
460317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
460318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
460318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
462683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
463474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
463477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
463478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
463478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
463479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
465856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
466651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
466654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
466655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
466656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
466656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
469023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
469812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
469815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
469816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
469816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
469817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
472178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
472967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
472974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
472976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
472976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
472977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
475368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
476159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
476162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
476164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
476164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
476165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
478546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
479334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
479345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
479346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
479347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
479347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
481715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
482506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
482508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.81ns 
482509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
482509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
482510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
484900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
485686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
485693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
485694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
485694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
485695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
488055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
488841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
488843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.12ns 
488846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
488846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.8ns 
488847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
491236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
492003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
492005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.82ns 
492006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
492006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
492007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
494398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
495183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
495188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
495189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
495189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
495190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
497545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
498332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
498335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
498336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
498337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
498337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
500735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
501524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
501528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
501529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
501529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
501530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
503895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
504680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
504684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
504685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
504685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
504686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
507068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
507854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
507859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
507860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
507860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
507861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
510229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
511020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
511034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ms 
511035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
511035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
511036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
513439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
514235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
514251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
514252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
514252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
514253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
516642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
517431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
517441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
517442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
517442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
517443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
519848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
520640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
520651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
520652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
520652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
520653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
523035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
523824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
523848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.17ms 
523850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
523850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
523850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
526242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
527033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
527057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
527058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
527058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
527059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
529427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
530216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
530238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.05ms 
530240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
530240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
530240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
532630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
533420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
533433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
533435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
533435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
533435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
535800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
536587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
536617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.22ms 
536618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
536618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
536619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
539005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
539795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
539840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.28ms 
539841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
539841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
539842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
542234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
543003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
543039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.13ms 
543041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
543041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
543041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
545422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
546208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
546248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.85ms 
546250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
546250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
546251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
548647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
549434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
549477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.9ms 
549478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
549478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
549479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
551846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
552636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
552751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.02ms 
552753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
552753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
552754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
555144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
555934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
555942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
555943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
555944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
555944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
558323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
559110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
559117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
559118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
559118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
559119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
561480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
562266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
562271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
562273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
562273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
562273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
564648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
565432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
565450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
565452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
565452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
565452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
567824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
568609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
568620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
568621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
568621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
568622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
570979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
571770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
571773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
571774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
571775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
571775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
574168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
574961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
574978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
574979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
574979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
574980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
577364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
578153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
578170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.15ms 
578171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
578171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
578172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
580560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
581328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
581347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
581348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
581348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
581349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
583741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
584528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
584531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
584533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
584533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
584533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
586914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
587706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
587709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
587711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
587711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
587711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
590096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
590884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
590890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
590892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
590892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
590892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
593262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
594049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
594055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
594057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
594057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
594058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
596438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
597227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
597294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.73ms 
597296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
597296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
597297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
599690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
600480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
600505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.17ms 
600507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
600507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
600507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
602884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
603677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
603698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.63ms 
603699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
603699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
603700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
606087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
606878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
606880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297.41ns 
606881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
606881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
606882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
609284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
610054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
610276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 210.68ms 
610279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
610279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.4ns 
610280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
612688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
613460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
613514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.08ms 
613518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
613519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
613519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
615910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
616699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
616701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.11ns 
616703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
616704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.8ns 
616704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
619086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
619874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
619876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.41ns 
619878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
619878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
619878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
622251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
623038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
623040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.71ns 
623041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
623041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
623042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
625416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
626202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
626204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.61ns 
626205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
626206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
626206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
628576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
629364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
629482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.19ms 
629485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
629485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.5ns 
629486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
631908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
632713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
632767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.67ms 
632769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
632769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
632771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
635197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
635992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
635994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
636019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
636080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
636102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
636110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
636119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
636122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
636124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
636127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
636131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
636133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
636138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
636140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
636363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
636364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
636365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
636366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
636367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
636474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
636475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
636476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
636477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
636478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
636479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
636638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
636639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
636640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
636641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
636642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
636642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
636770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
636771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
636772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
636773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
636774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
636775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
636781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
636782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
636783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
636784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
636785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
636786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
636792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
636793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
636794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
636795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
636796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
636797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
636932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
636933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
636934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
637064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
637065     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)'' 
637068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
637069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
637070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
637070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
637071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
637072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
637076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
637077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
637079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
637079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
637080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
637198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
637202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
637203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
637204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
637205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
637206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
637207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
637336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
637338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
637338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
637340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
637340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
637341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
637341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
637343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
637445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
637446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
637562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
637566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
637571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
637573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
637573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
637574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
637575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
637575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
637576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
637577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
637586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
637591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
637705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
637707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
637708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
637709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
637709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
637710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
637710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
637711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
637777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
637783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
637898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
637899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
637901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
637902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
637903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
637904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
638062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
638066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
638067     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)'' 
638069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
638070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
638070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
638071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
638072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
638081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
638083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
638084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
638084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
638188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
638190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
638190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
638191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
638192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
638192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
638299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
638300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
638301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
638302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
638303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
638303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
638304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
638305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
638391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
638393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
638470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
638471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
638472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
638476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
638480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
638485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
638606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
638608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
638609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
638610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
638658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
638740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
642277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
642278     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)'' 
642283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
642284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
642284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
642285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
642286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
642293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
642295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
642296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
642297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
642298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
642390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
642394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
642395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
642396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
642397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
642397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
642398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
642493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
642494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
642495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
642497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
642497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
642498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
642499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
642500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
642575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
642576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
642649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
642654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
642658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
642660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
642661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
642662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
642672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
642757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
642759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
642759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
642761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
642834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
642844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
642845     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)'' 
642847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
642848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
642849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
642850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
642850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
642861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
642863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
642864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
642865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
642866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
642996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
642997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
642999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
642999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
643000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
643090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
643095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
643096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
643097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
643098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
643098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
643099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
643197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
643199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
643200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
643201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
643202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
643203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
643203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
643204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
643205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
643206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
643207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
643208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
643208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
643209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
643210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
643296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
643297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
643304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
643380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
643459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
643460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
643461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
643462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
643463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
643463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
643464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
643464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
643465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
643549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
643555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
643644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
643645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
643645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
643646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
643647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
643647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
643648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
643648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
643654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
643654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
643733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
643738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
643744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
643842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
643843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
643844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
643845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
643846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
643846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
643846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
643847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
643901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
643902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
643903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
643904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
643905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
643910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
643915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
644034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
644121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
644123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
644123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
644124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
644290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
644377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
644378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
647515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
647520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
647521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
647521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
647522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
647636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
647637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
647638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
647639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
647640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
647748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
650847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
654055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
654059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
654060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
654061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
654062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
654175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
654176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
654177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
654178     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)' ...' 
654180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
655350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
655350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
655351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
657808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
658625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
658627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
658627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
658633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
658644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
658647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
658648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
658649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
658653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
658654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
658657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
658659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
658660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
658668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
658669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
658670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
658713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
658714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
658715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
658715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
658716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
658782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
658783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
658785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
658786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
658786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
658790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
658791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
658791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
658792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
658793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
658794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
658880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
658880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
658881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
658882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
658883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
658883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
658975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
658975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
658976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
658977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
658977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
658978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
658979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
658979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
658980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
658981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
658981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
658982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
658982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
658983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
658984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
658984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
658985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
658986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
658987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
658989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
659104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
659105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
659157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
659159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
659160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
659162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
659162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
659163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
659213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
659215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
659216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
659218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
659219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
659220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
659220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
659261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
659264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
659267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
659315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
659368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
659368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
659369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
661751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
662568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
662599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.77ms