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

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

tests
0

failures
0

ignored
10m55.27s

duration
100%

successful

Tests

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

Standard output

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

1498       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1500       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1503       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1503       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2909       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8301       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.71s 
8363       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8396       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.7ns 
8410       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8411       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 612.81ns 
8415       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
11271      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12273      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.04ms 
12288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12289      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 691.71ns 
12292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
15100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16017      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.92ms 
16019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16019      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
16020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
18639      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19573      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ms 
19577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 
19578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
22144      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23006      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
23012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 998.41ns 
23017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
25508      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms 
26362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142ns 
26363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
28831      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29761      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.05ms 
29764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
29765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
32243      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 658.61ns 
33093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.8ns 
33094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.81ns 
36401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
36402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
38888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39697      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.21ns 
39698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
39699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
42123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42929      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.41ns 
42931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.4ns 
42933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
45377      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46156      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 579.01ns 
46158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.4ns 
46159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
48620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49446      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.12ms 
49448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
49449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
51887      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52705      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.54ms 
52707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52708      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.2ns 
52709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
55139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56098      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 169.95ms 
56101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns 
56102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
58559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59342      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
59344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59344      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 
59345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
61800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
62584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62584      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.31ns 
62586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
65031      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.83ms 
65882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.9ns 
65883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
68323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69138      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.85ms 
69141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.31ns 
69143      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
71549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.34ms 
72377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.43ms 
72383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
74795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75605      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
75608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.4ns 
75609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
78017      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.58ms 
78828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.9ns 
78830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
81244      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82062      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.43ms 
82065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.9ns 
82066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
84473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85276      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
85279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.3ns 
85281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
87680      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88510      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.72ms 
88513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88513      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.1ns 
88514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
90928      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.59ms 
91776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.81ns 
91778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
94172      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.69ms 
95005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121ns 
95006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
97403      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98201      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
98203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
98204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
100592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
101401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
101414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
101416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
101417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 
101418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
103809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
104610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.8ns 
104612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
107004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
107810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
107810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
110210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
111010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.3ns 
111011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
113415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
114203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
114210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
114212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
114213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.2ns 
114214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
116607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
117403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
117406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
117407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
117407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
117408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
119837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
120631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
120642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
120643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
120643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
120644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
123032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
123818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
123866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.91ms 
123867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
123867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
123868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
126289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
127055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
127072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
127073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
127073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
127074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
129485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
130249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
130266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
130267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
130267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
130268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
132676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
133439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
133456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
133458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
133458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
133458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
135873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
136661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
136662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
136662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
136663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
139076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
139840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
139877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.11ms 
139879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
139879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.6ns 
139880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
142314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
143077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
143080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
143086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
143086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
143088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
145509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
146271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
146275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
146276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
146276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
146277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
148678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
149446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
149483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.76ms 
149485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
149485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
149485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
151883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
152681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
152682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
152682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
152683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
155064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
155850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
155867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms 
155868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
155868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
155869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
158254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
159038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
159045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
159047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
159047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
159047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
161474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
162265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
162268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
162269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
162269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
162270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
164656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
165440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
165443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
165444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
165445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
165445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
167829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
168614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
168618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
168619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
168619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
168620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
171014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
171801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
171865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.38ms 
171867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
171867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
171868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
174250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
175034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
175104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.16ms 
175105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
175106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
175106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
177484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
178269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
178272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
178274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
178274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
178274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
180651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
181437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
181470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.36ms 
181471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
181472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.3ns 
181472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
183860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
184645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
184670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
184672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
184672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
184673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
187059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
187843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
187846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
187847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
187847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
187848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
190221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
191004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
191128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.24ms 
191130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
191131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns 
191131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
193513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
194297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
194307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
194308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
194308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
194309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
196687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
197471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
197478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
197479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
197479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
197480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
199876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
200639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
200654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
200655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
200655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
200656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
203056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
203817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
203828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
203830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
203831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
203831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
206219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
206979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
206982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
206984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
206984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
206984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
209381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
210143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
210147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
210149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
210149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
210149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
212547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
213307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
213327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.79ms 
213328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
213328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
213329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
215744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
216508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
216523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
216524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
216524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
216525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
218928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
219694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
219708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.41ms 
219709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
219709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
219710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
222121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
222886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
222889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
222891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
222891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
222891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
225300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
226064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
226095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.65ms 
226097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
226097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
226097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
228477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
229263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
229268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
229269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
229269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
229270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
231653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
232439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
232442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
232443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
232444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
232444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
234828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
235613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
235615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.01ns 
235616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
235616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
235617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
237997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
238781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
238784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
238786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
238786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
238786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
241172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
241956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
241958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 896.51ns 
241960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
241960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
241961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
244343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
245126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
245196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.16ms 
245198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
245199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 515.31ns 
245200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
247597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
248382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
248417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.31ms 
248418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
248418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
248419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
250809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
251593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
251629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.98ms 
251633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
251633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260ns 
251634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
254016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
254800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
254844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.99ms 
254845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
254846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
254846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
257239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
258025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
258058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.12ms 
258059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
258059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
258060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
260447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
261234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
261283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.79ms 
261285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
261285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
261286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
263676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
264507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
264508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
264508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.3ns 
264509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
266897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
267683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
267702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.31ms 
267703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
267703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
267704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
270096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
270881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
270904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.76ms 
270905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
270905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
270906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
273285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
274073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
274092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.67ms 
274093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
274093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
274094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
276483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
277269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
277294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.5ms 
277295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
277295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
277296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
279703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
280465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
280490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 
280492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
280496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
280497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
282906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
283692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.31ms 
283693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
283693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
283694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
286099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
286861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
286884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.15ms 
286885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
286885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
286886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
289287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
290047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
290072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
290074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
290074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.7ns 
290075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
292476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
293241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
293268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.93ms 
293270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
293270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.3ns 
293271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
295680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
296442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
296465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
296467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
296467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
296467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
298867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
299661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
299671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
299672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
299672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
299673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
302054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
302856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 
302857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
302857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
302858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
305231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
306018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
306022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
306024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
306024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 
306025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
308405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
309189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
309191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.31ns 
309192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
309192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
309193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
311564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
312348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
312350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.61ns 
312354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
312354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.7ns 
312355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
314730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
315515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
315521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
315522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
315522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
315523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
317931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
318721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
318727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
318729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
318729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
318730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
321117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
321917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
321918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
321919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
321919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
324307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
325095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
325098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
325099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
325099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
325100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
327472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
328258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
328260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.31ns 
328261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
328261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
328262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
330639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
331424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
331429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
331430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
331430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
331431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
333809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
334595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
334597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.11ns 
334599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
334599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.7ns 
334600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
336988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
337776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
337778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.71ns 
337779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
337779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
337780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
340160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
340945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
340947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.41ns 
340949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
340949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
340949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
343327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
344119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
344122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
344124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
344124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
344124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
346502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
347286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
347295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
347296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
347296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
347297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
349674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
350460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
350464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
350465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
350465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
350466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
352847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
353633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
353640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
353641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
353641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
353642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
356022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
356805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
356809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
356810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
356810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
356811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
359206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
359969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
359985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
359986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
359986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
359987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
362390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
363153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
363156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
363158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
363158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
363158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
365565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
366328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
366331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
366332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
366332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
366332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
368734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
369497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
369501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
369502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
369502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
369503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
371909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
372673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
372689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.38ms 
372690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
372690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
372691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
375089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
375850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
375854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 505.91ns 
375855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
375856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
375856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
378248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
379011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
379047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.38ms 
379049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
379049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
379050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
381441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
382202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
382206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
382207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
382207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
382208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
384600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
385362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
385415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50ms 
385417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
385418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.8ns 
385418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
387798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
388583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
388603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.81ms 
388604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
388604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
388605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
390988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
391776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
391798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
391799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
391799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
391800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
394187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
394971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
394973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513.41ns 
394974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
394974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
394975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
397352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
398141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
398147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
398148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
398148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
398149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
400526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
401315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
401319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
401321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
401321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
401322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
403718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
404509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
404511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.01ns 
404512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
404512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
404513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
406890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
407679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
407682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.31ns 
407683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
407683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
407683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
410054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
410847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
410850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
410851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
410851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
410852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
413227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
414019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
414022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
414023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
414023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
414024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
416398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
417195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
417204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ms 
417206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
417206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
417207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
419579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
420370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
420382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.37ms 
420383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
420383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
420384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
422762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
423560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
423570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
423572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
423572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
423572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
425967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
426741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
426753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
426754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
426755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
426755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
429148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
429924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
429928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
429929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
429929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
429930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
432333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
433128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
433135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
433136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
433136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
433136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
435528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
436332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
436334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.31ns 
436335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
436335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
436336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
438706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
439503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
439505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
439507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
439507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
439507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
441882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
442680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
442683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 783.01ns 
442684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
442684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
442685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
445080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
445881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
445891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
445893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
445893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.1ns 
445894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
448290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
449087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
449091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
449092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
449092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
449093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
451493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
452268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
452274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
452276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
452276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
452276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
454668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
455471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
455473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.51ns 
455474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
455474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
455475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
457850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
458647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
458649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.91ns 
458650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
458651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
458651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
461027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
461829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
461833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
461835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
461835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.3ns 
461836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
464233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
465034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
465037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
465039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
465039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
465039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
467430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
468204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
468207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
468208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
468208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
468209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
470600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
471397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
471400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
471401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
471401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
471402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
473773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
474571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
474576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
474577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
474577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
474578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
476946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
477744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
477747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
477748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
477748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
477749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
480119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
480917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
480927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.24ms 
480928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
480929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
480929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
483323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
484099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
484101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.71ns 
484102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
484102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
484103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
486508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
487307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
487314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
487315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
487315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
487316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
489698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
490497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
490499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 902.61ns 
490500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
490501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
490501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
492894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
493669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
493671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.51ns 
493672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
493672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
493673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
496070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
496869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
496873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
496875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
496875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
496875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
499250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
500050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
500054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
500055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
500055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
500056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
502432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
503232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
503235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
503236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
503236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
503237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
505631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
506427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
506431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
506432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
506432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
506433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
508806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
509610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
509615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
509616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
509616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
509617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
511988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
512787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
512800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
512801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
512801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
512802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
515198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
515997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
516012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
516013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
516013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
516014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
518391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
519190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
519200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
519201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
519201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
519202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
521602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
522389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
522401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
522403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
522403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
522403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
524803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
525600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
525624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
525625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
525625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
525625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
527997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
528797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
528821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
528822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
528822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
528823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
531215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
532014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
532036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.81ms 
532037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
532037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
532038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
534416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
535214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
535227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
535228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
535229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
535229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
537619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
538395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
538423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.06ms 
538424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
538424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
538425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
540821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
541623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
541667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.97ms 
541668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
541669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
541669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
544066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
544845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
544881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.95ms 
544882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
544882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
544883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
547278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
548077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
548116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.94ms 
548117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
548118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
548118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
550490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
551290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
551331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.94ms 
551332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
551332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
551333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
553735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
554536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
554648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.28ms 
554649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
554649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
554650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
557056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
557835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
557843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
557844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
557844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
557845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
560238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
561035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
561043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
561044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
561044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
561045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
563439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
564216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
564221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
564222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
564222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
564223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
566613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
567413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
567430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
567432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
567432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
567433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
569820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
570688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
570699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
570700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
570700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
570701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
573088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
573884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
573887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
573888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
573888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
573888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
576279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
577084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
577100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms 
577101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
577101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
577101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
579476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
580274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
580289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.01ms 
580291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
580291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
580292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
582682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
583482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
583501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.55ms 
583502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
583502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
583502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
585868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
586666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
586669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
586670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
586670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
586671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
589091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
589912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
589916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
589917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
589917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
589918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
592302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
593078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
593085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
593087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
593087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
593088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
595499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
596296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
596301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
596302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
596302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
596303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
598695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
599494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
599559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.04ms 
599560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
599560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
599561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
601965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
602744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
602769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.29ms 
602771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
602771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
602771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
605181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
605981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
606002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
606003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
606003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
606004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
608412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
609211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
609214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 302.5ns 
609215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
609215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.2ns 
609217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
611609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
612386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
612610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 213.54ms 
612612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
612612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.5ns 
612613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
614987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
615789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
615837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.64ms 
615839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
615839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
615840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
618229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
619029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
619031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.5ns 
619032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
619032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
619032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
621423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
622220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
622222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.8ns 
622223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
622223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
622224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
624615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
625393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
625395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 341.7ns 
625396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
625396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
625397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
627779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
628576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
628578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 494.61ns 
628579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
628579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
628580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
630981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
631781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
631869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.12ms 
631871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
631871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.5ns 
631873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
634279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
635079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
635128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.95ms 
635130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
635130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
635131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
637537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
638336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
638337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
638363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
638396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
638412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
638416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
638422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
638424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
638425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
638427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
638430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
638432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
638434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
638435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
638636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
638637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
638639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
638640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
638641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
638744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
638746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
638747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
638748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
638749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
638750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
638892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
638894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
638895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
638896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
638896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
638898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
639011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
639013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
639014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
639015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
639016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
639016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
639023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
639024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
639025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
639026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
639028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
639028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
639034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
639035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
639037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
639038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
639038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
639039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
639161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
639162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
639164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
639281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
639282     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)'' 
639285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
639286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
639287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
639288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
639289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
639290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
639295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
639296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
639297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
639298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
639404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
639408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
639410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
639411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
639412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
639413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
639414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
639524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
639526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
639527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
639528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
639529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
639530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
639531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
639532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
639613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
639615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
639699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
639706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
639714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
639715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
639716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
639718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
639718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
639719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
639720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
639721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
639732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
639739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
639858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
639860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
639861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
639862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
639863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
639863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
639864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
639865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
639917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
639922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
640018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
640019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
640021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
640023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
640024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
640025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
640146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
640150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
640152     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)'' 
640154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
640155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
640156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
640157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
640157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
640166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
640167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
640168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
640169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
640257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
640258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
640259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
640260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
640261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
640262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
640354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
640356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
640357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
640359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
640360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
640360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
640361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
640362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
640437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
640439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
640524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
640525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
640526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
640530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
640534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
640542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
640655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
640658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
640659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
640660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
640670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
640750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
644166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
644167     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)'' 
644172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
644173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
644174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
644174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
644175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
644182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
644183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
644185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
644185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
644186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
644274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
644278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
644279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
644280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
644281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
644281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
644282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
644372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
644373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
644374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
644375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
644376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
644377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
644377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
644378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
644450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
644452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
644521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
644525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
644529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
644530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
644531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
644532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
644541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
644616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
644617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
644618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
644619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
644688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
644697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
644698     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)'' 
644700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
644701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
644702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
644702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
644703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
644713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
644714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
644715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
644716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
644717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
644801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
644803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
644804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
644805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
644806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
644892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
644896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
644897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
644898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
644898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
644899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
644900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
644993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
644995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
644996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
644997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
644998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
644999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
644999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
645000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
645001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
645002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
645003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
645004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
645004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
645005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
645006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
645088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
645090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
645096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
645170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
645331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
645332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
645334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
645334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
645335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
645336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
645336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
645337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
645338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
645420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
645425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
645510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
645511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
645512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
645513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
645514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
645514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
645514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
645515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
645519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
645520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
645596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
645600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
645605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
645699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
645700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
645701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
645702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
645702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
645703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
645703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
645704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
645756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
645757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
645757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
645758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
645759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
645764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
645768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
645879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
645963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
645964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
645965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
645966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
646127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
646211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
646212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
649126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
649131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
649132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
649132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
649133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
649243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
649244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
649245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
649245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
649246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
649347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
652184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
655221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
655225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
655226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
655227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
655227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
655336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
655337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
655338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
655339     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)' ...' 
655341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
656446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
656446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
656446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
658954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
659779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
659780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
659782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
659788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
659798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
659801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
659803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
659803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
659807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
659808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
659810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
659813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
659813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
659821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
659822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
659823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
659863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
659864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
659865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
659865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
659866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
659933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
659935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
659936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
659936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
659939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
659940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
659940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
659941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
659942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
659942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
660027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
660028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
660028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
660030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
660030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
660031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
660117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
660118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
660119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
660119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
660120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
660121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
660121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
660122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
660123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
660123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
660124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
660124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
660125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
660125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
660126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
660126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
660127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
660128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
660129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
660131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
660165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
660166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
660214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
660215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
660217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
660218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
660219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
660219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
660257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
660259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
660260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
660262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
660263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
660264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
660264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
660304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
660306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
660309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
660356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
660407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
660407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
660408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
662825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
663655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
663685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.6ms