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

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

tests
0

failures
0

ignored
10m48.64s

duration
100%

successful

Tests

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

Standard output

657        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
677        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.61ms 
875        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
889        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)

1687       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1690       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1695       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1696       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3177       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8360       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.48s 
8415       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8446       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.7ns 
8458       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8459       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.1ns 
8463       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
11314      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12223      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
12232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.7ns 
12236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
14929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
15793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15793      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
15795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
18490      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19341      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
19347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19348      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.8ns 
19353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
21879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22702      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
22704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
22705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
25154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26006      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.06ms 
26013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.7ns 
26014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
28479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29302      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms 
29305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29306      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.6ns 
29307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
31776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.21ns 
32636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 611ns 
32638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
35076      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35852      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.4ns 
35854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.5ns 
35856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
38320      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.81ns 
39125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.71ms 
39131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41556      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
41556      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42352      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.3ns 
42354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.5ns 
42356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
44764      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
45571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.5ns 
45573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47984      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
47984      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48814      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.4ms 
48816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 
48820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
51236      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52037      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.48ms 
52046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 618.71ns 
52048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54473      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
54473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55497      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 208.22ms 
55501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388ns 
55503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57992      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
57992      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58809      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
58811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 
58812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
61199      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
61988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
61989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
64367      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65194      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.52ms 
65196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.4ns 
65198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
67652      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68433      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ms 
68434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
68435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
70841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71641      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.47ms 
71643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
71644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
74043      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74843      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
74845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
74846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
77245      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78047      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
78050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.2ns 
78051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
80426      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
81241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.3ns 
81242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
83631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84390      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
84392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
84393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
86784      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87606      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.57ms 
87608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.2ns 
87609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
89983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90819      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.47ms 
90822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.3ns 
90823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
93200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94036      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.16ms 
94042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94044      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.82ms 
94046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
96430      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97219      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.42ms 
97221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97221      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
97222      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
99617      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
100389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
100390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
102803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
103599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.8ns 
103601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
105985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
106790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.7ns 
106791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
109166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
109964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.8ns 
109965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
112351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
113149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
113150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
115553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
116321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.1ns 
116322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
118717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
119511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.3ns 
119513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
121884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.37ms 
122718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.5ns 
122720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
125105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
125901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.5ns 
125902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
128263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
129058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
129059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
131436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ms 
132207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
132208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
134586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
135362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
135380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
135381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
137798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.56ms 
138632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
138633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
141000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
141779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
141780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
144156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
144915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
144916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
147294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
148056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
148057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
150441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
151298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
151306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
151307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
151307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
151308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
153666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
154445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
154480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.31ms 
154494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
154494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns 
154495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
156866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.68ms 
157658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.11ms 
157666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
160027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
160808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.4ns 
160809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
163197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
163953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
163953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
166327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
167106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
167110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
167111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
167111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
167112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
169468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
170245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
170355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.43ms 
170361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
170361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.4ns 
170363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
172735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
173512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
173595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.09ms 
173597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
173597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.5ns 
173598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
175987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
176749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.5ns 
176750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
179141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.95ms 
179958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.2ns 
179960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
182319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
183095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
183130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.18ms 
183133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
183133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.7ns 
183134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
185500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
186275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
186278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
186279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
186279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
186280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
188630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
189402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.12ms 
189540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.1ns 
189542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
191935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
192697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.4ns 
192698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
195082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
195866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.2ns 
195866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
198218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
199006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms 
199007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
199007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
199008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
201352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
202124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
202135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
202137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
202137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
202138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
204488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
205264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
205267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
205268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
205268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
205269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
207643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
208395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
208399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
208400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
208400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
208401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
210783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ms 
211591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.3ns 
211593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
213961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
214759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
214760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
217117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.07ms 
217913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
217914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
220275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
221051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
221055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
221056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
221056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
221057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
223432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
224183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
224187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
224189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
224189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.8ns 
224190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
226555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
227329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
227334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
227335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
227336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
227336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
229683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
230453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
230456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
230457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
230457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
230458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
232808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
233581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
233584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.21ns 
233585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
233585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
233586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
235931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
236705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
236709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
236710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
236710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
236711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
239085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
239835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
239838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.21ns 
239839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
239839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
239840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
242208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
242988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
243052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.73ms 
243054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
243054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
243055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
245423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
246199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
246242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.01ms 
246243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
246244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.6ns 
246245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
248626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
249399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
249431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.56ms 
249432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
249432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
249433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
251781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
252552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
252591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.01ms 
252592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
252592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
252593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
254964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
255713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
255741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
255742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
255742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
255743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
258120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
258894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
258939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.33ms 
258941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
258941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
258941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
261292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
262067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
262113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.05ms 
262114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
262114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
262115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
264464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
265239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
265258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
265259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
265259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
265260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
267643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
268394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
268417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
268419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
268419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
268419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
270794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
271545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
271563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.68ms 
271565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
271565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
271565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
273976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
274750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
274776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.07ms 
274778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
274778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
274779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
277133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
277912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
277936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
277937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
277937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
277938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
280293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
281069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
281093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
281094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
281094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
281095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
283464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
284214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
284237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.35ms 
284238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
284238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
284239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
286635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
287407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
287427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.99ms 
287428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
287429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
287429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
289800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
290577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
290600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.95ms 
290601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
290601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
290602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
292962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
293735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
293758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.93ms 
293760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
293760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
293760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
296115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
296894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
296902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 
296903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
296903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
296904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
299290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
300041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
300059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
300060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
300060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
300061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
302435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
303213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
303217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
303218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
303218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
303219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
305578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
306355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
306358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
306359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
306359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
306360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
308726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
309506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
309508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.11ns 
309510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
309510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
309510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
311868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
312666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
312674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
312675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
312675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
312678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
315063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
315814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
315820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
315822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
315822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
315822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
318212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
318991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
319003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
319005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
319005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
319005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
321368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
322148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
322151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
322152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
322152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
322153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
324508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
325283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
325285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 507.9ns 
325287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
325287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
325287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
327640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
328415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
328420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
328421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
328421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
328422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
330802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
331558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
331560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549ns 
331561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
331561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
331562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
333942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
334719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
334722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.8ns 
334724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
334724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.7ns 
334725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
337083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
337861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
337863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.31ns 
337864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
337864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
337865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
340226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
341004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
341008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
341009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
341009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
341010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
343359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
344136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
344145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
344146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
344146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
344147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
346514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
347265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
347269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
347271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
347271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
347271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
349643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
350418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
350425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
350426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
350426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
350427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
352783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
353561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
353568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
353572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
353572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 759.71ns 
353573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
355936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
356710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
356725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
356727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
356727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
356727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
359111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
359891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
359894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
359895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
359895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
359896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
362263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
363014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
363018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
363019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
363019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
363020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
365385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
366159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
366163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
366164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
366164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
366165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
368523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
369300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
369316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
369317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
369317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
369318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
371679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
372454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
372458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 501.81ns 
372460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
372460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
372461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
374808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
375581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
375619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.81ms 
375620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
375620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
375621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
377999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
378753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
378756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
378757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
378757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
378758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
381132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
381907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
381928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.35ms 
381929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
381929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
381930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
384292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
385073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
385095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.61ms 
385096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
385096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
385097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
387456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
388235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
388259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.81ms 
388261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
388261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
388261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
390670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
391427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
391430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.91ns 
391431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
391431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
391432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
393811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
394587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
394593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
394594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
394594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
394595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
396950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
397728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
397731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
397732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
397732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
397733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
400090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
400873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
400875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.41ns 
400876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
400876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
400877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
403251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
404006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
404008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.61ns 
404009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
404009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
404010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
406384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
407166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
407169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
407170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
407170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
407171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
409524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
410307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
410310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
410312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
410313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
410313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
412690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
413448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
413458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
413459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
413459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
413460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
415833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
416616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
416628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 
416630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
416630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
416630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
418992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
419803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
419816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
419817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
419817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
419818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
422196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
422964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
422975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
422977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
422977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
422977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
425354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
426142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
426147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
426148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
426148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
426149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
428507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
429294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
429301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
429302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
429302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
429302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
431684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
432451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
432453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.51ns 
432454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
432454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
432455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
434832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
435622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
435625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
435626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
435626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
435627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
437982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
438771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
438774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.81ns 
438775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
438775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
438776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
441152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
441938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
441949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
441950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
441950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
441951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
444323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
445113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
445117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
445118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
445118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
445119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
447501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
448268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
448274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
448276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
448276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
448276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
450659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
451447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
451449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.51ns 
451451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
451451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
451451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
453825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
454592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
454594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.11ns 
454595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
454595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
454596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
456969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
457756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
457760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
457761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
457762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 
457762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
460115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
460905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
460907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
460909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
460909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
460909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
463279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
464067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
464070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
464071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
464071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
464072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
466430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
467217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
467220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
467221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
467221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
467222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
469595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
470380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
470385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
470387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
470387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
470387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
472739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
473527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
473530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
473532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
473532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
473532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
475911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
476697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
476708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
476709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
476710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
476710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
479073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
479863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
479865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.41ns 
479866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
479866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
479867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
482241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
483029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
483036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
483037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
483037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
483038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
485417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
486183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
486186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.71ns 
486187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
486187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
486188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
488561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
489350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
489352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.11ns 
489353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
489354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
489354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
491746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
492533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
492537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
492539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
492539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
492539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
494900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
495705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
495708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
495710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
495710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.8ns 
495711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
498084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
498871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
498875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
498876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
498876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
498877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
501247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
502016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
502020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
502021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
502021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
502022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
504396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
505185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
505190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
505191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
505191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
505192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
507570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
508357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
508371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms 
508372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
508372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
508373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
510735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
511522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
511537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.01ms 
511538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
511538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
511539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
513911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
514699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
514709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
514710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
514710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
514711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
517083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
517872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
517882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
517884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
517884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
517885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
520244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
521030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
521056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.92ms 
521057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
521057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
521058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
523428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
524215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
524240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
524242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
524242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
524242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
526614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
527403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
527426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
527427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
527427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
527428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
529804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
530595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
530609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
530610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
530610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
530611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
532974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
533764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
533796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.96ms 
533797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
533797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
533798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
536178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
536968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
537016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.46ms 
537017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
537018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
537018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
539398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
540185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
540223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.57ms 
540225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
540225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
540225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
542599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
543389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
543431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.09ms 
543432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
543432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
543433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
545808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
546577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
546621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.35ms 
546622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
546622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
546623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
549004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
549796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
549915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.89ms 
549916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
549916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
549917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
552310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
553103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
553110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
553112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
553112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
553112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
555490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
556280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
556288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
556289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
556289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
556290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
558669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
559460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
559465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
559466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
559466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
559467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
561848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
562636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
562654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ms 
562655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
562655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
562656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
565015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
565806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
565817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
565818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
565818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
565819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
568199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
568964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
568968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
568969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
568969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
568969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
571329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
572117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
572133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
572134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
572134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
572135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
574494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
575279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
575295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.26ms 
575296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
575296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
575297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
577668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
578454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
578473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.52ms 
578475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
578475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
578475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
580847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
581635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
581638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
581639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
581639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
581640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
584007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
584794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
584797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
584798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
584798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
584799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
587160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
587948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
587954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
587955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
587955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
587956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
590326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
591115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
591121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
591122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
591122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
591123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
593490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
594279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
594348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.79ms 
594349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
594349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
594350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
596739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
597530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
597556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.68ms 
597557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
597557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
597558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
599944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
600736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
600758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
600759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
600759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
600760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
603136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
603929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
603931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 354.6ns 
603933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
603933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
603934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
606319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
607105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
607303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.85ms 
607305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
607306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.3ns 
607306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
609681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
610474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
610529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.57ms 
610533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
610533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
610534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
612930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
613696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
613698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 324ns 
613699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
613699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
613700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
616086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
616875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
616877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 350.7ns 
616879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
616879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
616879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
619237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
620026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
620028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.2ns 
620031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
620031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
620032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
622388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
623177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
623179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 494.81ns 
623180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
623180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
623181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
625531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
626320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
626413     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
626428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.53ms 
626431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
626431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
626432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
628815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
629604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
629665     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
629666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.66ms 
629667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
629667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
629668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
632041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
632840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
632842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
632868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
632917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
632943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
632950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
632956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
632959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
632961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
632964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
632969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
632971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
632977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
632978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
633192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
633194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
633195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
633196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
633197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
633325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
633327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
633330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
633332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
633334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
633335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
633479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
633481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
633482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
633483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
633485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
633488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
633591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
633593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
633594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
633595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
633596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
633597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
633604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
633605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
633606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
633609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
633611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
633612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
633619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
633621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
633622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
633623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
633623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
633624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
633742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
633745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
633748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
633850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
633853     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)'' 
633856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
633857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
633859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
633862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
633863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
633866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
633872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
633874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
633875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
633876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
633877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
634033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
634038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
634039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
634040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
634041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
634042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
634044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
634147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
634150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
634150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
634152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
634153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
634154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
634155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
634156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
634238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
634239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
634338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
634342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
634346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
634347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
634348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
634349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
634349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
634350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
634350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
634351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
634358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
634361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
634439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
634440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
634441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
634442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
634443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
634443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
634444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
634445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
634489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
634494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
634569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
634570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
634572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
634574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
634574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
634575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
634670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
634674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
634675     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)'' 
634677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
634677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
634678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
634679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
634679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
634686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
634688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
634692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
634693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
634767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
634768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
634769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
634771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
634771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
634773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
634852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
634854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
634854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
634856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
634856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
634857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
634858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
634859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
634924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
634925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
634989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
634990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
634990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
634994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
634998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
635001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
635104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
635106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
635107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
635108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
635116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
635186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
638411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
638412     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)'' 
638417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
638418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
638418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
638419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
638420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
638426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
638427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
638428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
638429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
638429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
638511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
638514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
638515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
638516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
638517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
638517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
638518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
638600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
638601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
638602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
638603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
638604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
638604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
638605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
638606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
638673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
638674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
638738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
638741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
638745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
638746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
638747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
638748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
638756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
638827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
638828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
638829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
638830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
638894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
638902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
638902     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)'' 
638904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
638905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
638905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
638906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
638906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
638916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
638917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
638918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
638918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
638919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
638996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
638997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
638998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
638999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
639000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
639082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
639086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
639087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
639088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
639088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
639089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
639090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
639177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
639178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
639179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
639180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
639181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
639181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
639182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
639183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
639184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
639184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
639185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
639186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
639186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
639186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
639187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
639265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
639266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
639271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
639341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
639413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
639414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
639415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
639415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
639416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
639417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
639417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
639417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
639418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
639496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
639501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
639580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
639581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
639582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
639583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
639583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
639584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
639584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
639585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
639589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
639590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
639702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
639707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
639711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
639797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
639798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
639799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
639801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
639801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
639802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
639849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
639850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
639851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
639852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
639852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
639857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
639862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
639968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
640044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
640045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
640046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
640047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
640195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
640272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
640272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
643019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
643024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
643025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
643025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
643026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
643126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
643127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
643128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
643129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
643130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
643222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
645880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
648702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
648706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
648707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
648708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
648709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
648808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
648809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
648810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
648811     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)' ...' 
648812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
649835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
649835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
649836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
652262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
653089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
653090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
653090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
653099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
653113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
653115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
653117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
653118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
653122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
653124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
653127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
653130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
653131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
653141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
653143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
653144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
653219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
653220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
653220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
653221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
653221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
653284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
653285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
653288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
653288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
653289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
653292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
653293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
653293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
653294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
653295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
653296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
653367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
653368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
653369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
653370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
653371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
653371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
653448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
653449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
653449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
653450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
653451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
653452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
653452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
653453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
653454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
653454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
653455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
653455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
653464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
653464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
653465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
653465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
653466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
653467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
653468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
653470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
653505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
653507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
653612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
653613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
653614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
653615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
653616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
653616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
653660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
653662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
653663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
653664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
653666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
653666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
653666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
653710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
653712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
653715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
653766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
653816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
653816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
653817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
656249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
657090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
657121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.83ms