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

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

tests
0

failures
0

ignored
14m23.45s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.071s passed
powPositiveConcrete data()[101] 4.072s passed
powGeq1Concrete data()[102] 4.050s passed
pow2InIntLower data()[103] 4.072s passed
pow2InIntUpper data()[104] 4.158s passed
logSelfConcrete data()[105] 4.210s passed
log1Concrete data()[106] 4.221s passed
logProduct data()[107] 4.201s passed
logTimesBaseConcrete data()[108] 4.150s passed
logProdIdentity data()[109] 4.083s passed
moduloByteIsInByte data()[10] 4.181s passed
logProdIdentityConcrete data()[110] 4.196s passed
logPowIdentity data()[111] 4.250s passed
logPowIdentityConcrete data()[112] 4.265s passed
logPositive data()[113] 4.231s passed
logPositiveConcrete data()[114] 4.200s passed
logMono data()[115] 4.231s passed
logMonoConcrete data()[116] 4.145s passed
powLogLess data()[117] 4.166s passed
powLogMore2 data()[118] 4.186s passed
logLessThanPow data()[119] 4.233s passed
moduloCharIsInChar data()[11] 4.247s passed
logLessThanPowConcrete data()[120] 4.140s passed
logSqueeze data()[121] 4.151s passed
ifthenelse_equals data()[122] 4.147s passed
ifthenelse_equals_1 data()[123] 4.147s passed
ifthenelse_equals_2 data()[124] 4.150s passed
disjointWithSingleton1 data()[125] 4.132s passed
disjointWithSingleton2 data()[126] 4.116s passed
disjointArrayRanges data()[127] 4.165s passed
disjointArrayRangeAllFields1 data()[128] 4.161s passed
disjointArrayRangeAllFields2 data()[129] 4.144s passed
div_unique1 data()[12] 4.529s passed
seqSelfDefinition data()[130] 4.222s passed
seqOutsideValue data()[131] 4.201s passed
castedGetAny data()[132] 4.198s passed
seqGetAlphaCast data()[133] 4.124s passed
getOfSeqSingleton data()[134] 4.151s passed
getOfSeqSingletonConcrete data()[135] 4.157s passed
getOfSeqConcat data()[136] 4.275s passed
getOfSeqSub data()[137] 4.208s passed
getOfSeqReverse data()[138] 4.203s passed
lenOfSeqEmpty data()[139] 4.192s passed
div_unique2 data()[13] 4.306s passed
lenOfSeqSingleton data()[140] 4.202s passed
lenOfSeqConcat data()[141] 4.321s passed
lenOfSeqSub data()[142] 4.263s passed
lenOfSeqReverse data()[143] 4.205s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.128s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.213s passed
getOfSeqSingletonEQ data()[146] 4.133s passed
getOfSeqConcatEQ data()[147] 4.174s passed
getOfSeqSubEQ data()[148] 4.160s passed
getOfSeqReverseEQ data()[149] 4.120s passed
div_exists data()[14] 4.493s passed
lenOfSeqEmptyEQ data()[150] 4.103s passed
lenOfSeqSingletonEQ data()[151] 4.168s passed
lenOfSeqConcatEQ data()[152] 4.177s passed
lenOfSeqSubEQ data()[153] 4.169s passed
lenOfSeqReverseEQ data()[154] 4.206s passed
getOfSeqDefEQ data()[155] 4.207s passed
lenOfSeqDefEQ data()[156] 4.247s passed
seqConcatWithSeqEmpty1 data()[157] 4.192s passed
seqConcatWithSeqEmpty2 data()[158] 4.239s passed
seqReverseOfSeqEmpty data()[159] 4.205s passed
div_one data()[15] 4.338s passed
subSeqComplete data()[160] 4.281s passed
subSeqTailR data()[161] 4.277s passed
subSeqTailL data()[162] 4.273s passed
subSeqTailEQR data()[163] 4.331s passed
subSeqTailEQL data()[164] 4.276s passed
seqDef_split data()[165] 4.307s passed
seqDef_induction_upper data()[166] 4.360s passed
seqDef_induction_upper_concrete data()[167] 4.322s passed
seqDef_induction_lower data()[168] 4.377s passed
seqDef_induction_lower_concrete data()[169] 4.379s passed
jdiv_one data()[16] 4.260s passed
seqDef_split_in_three data()[170] 4.482s passed
seqDef_empty data()[171] 4.315s passed
seqDef_one_summand data()[172] 4.271s passed
seqDef_lower_equals_upper data()[173] 4.237s passed
seqDefOfSeq data()[174] 4.283s passed
seqSelfDefinitionEQ2 data()[175] 4.161s passed
indexOfSeqSingleton data()[176] 4.211s passed
indexOfSeqConcatFirst data()[177] 4.245s passed
indexOfSeqConcatSecond data()[178] 4.204s passed
indexOfSeqSub data()[179] 4.253s passed
div_zero data()[17] 4.174s passed
lenOfArray2seq data()[180] 4.204s passed
getAnyOfArray2seq data()[181] 4.223s passed
getOfArray2seq data()[182] 4.238s passed
getAnyOfNPermInv data()[183] 4.159s passed
seqNPermRange data()[184] 4.339s passed
seqPermTrans data()[185] 4.246s passed
seqPermRefl data()[186] 4.242s passed
seqPermSplit data()[187] 4.175s passed
seqNPermRight data()[188] 4.485s passed
seqPermFromSwap data()[189] 4.265s passed
divResZero1 data()[18] 4.185s passed
seqPermTransAlt0 data()[190] 4.179s passed
seqPermTransAlt1 data()[191] 4.176s passed
seqPermTransAlt2 data()[192] 4.248s passed
seqPermTransAlt3 data()[193] 4.250s passed
seqPermForall data()[194] 4.276s passed
seqPermExists data()[195] 4.226s passed
schiffl_lemma_2 data()[196] 30.026s passed
schiffl_thm_1 data()[197] 5.179s passed
eqSameSeq data()[198] 4.359s passed
divResZero2 data()[19] 4.205s passed
eqTermCut data()[1] 5.306s passed
divResOne1 data()[20] 4.122s passed
divResOne2 data()[21] 4.256s passed
div_cancel1 data()[22] 4.304s passed
div_cancel2 data()[23] 4.231s passed
divAddMultDenom data()[24] 4.226s passed
divMinus data()[25] 4.262s passed
divMinusDenom data()[26] 4.276s passed
divLeastDPos data()[27] 4.108s passed
divLeastDNeg data()[28] 4.217s passed
divGreatestDPos data()[29] 4.299s passed
equivAllRight data()[2] 4.838s passed
divGreatestDNeg data()[30] 4.195s passed
divIncreasingPos data()[31] 4.162s passed
divIncreasingNeg data()[32] 4.157s passed
jdiv_zero data()[33] 4.193s passed
jdivPulloutMinusNum data()[34] 4.130s passed
jdivPulloutMinusDenom data()[35] 4.214s passed
jdiv_uniquePosPos data()[36] 4.352s passed
jdiv_uniquePosNeg data()[37] 4.146s passed
jdiv_uniqueNegPos data()[38] 4.237s passed
jdiv_uniqueNegNeg data()[39] 4.297s passed
irrflConcrete1 data()[3] 4.576s passed
jdivMultDenom1 data()[40] 4.250s passed
jdivMultDenom2 data()[41] 4.229s passed
mod_geZero data()[42] 4.220s passed
mod_lessDenom data()[43] 4.101s passed
jmod_NumPos data()[44] 4.098s passed
jmod_NumNeg data()[45] 4.032s passed
jmod_geZero data()[46] 4.169s passed
jmodNumZero data()[47] 4.171s passed
jmod_pulloutminusNum data()[48] 4.195s passed
jmod_pulloutminusDenom data()[49] 4.282s passed
irrflConcrete2 data()[4] 4.445s passed
jmodUnique1 data()[50] 4.230s passed
jmodUnique2 data()[51] 4.285s passed
intDivRem data()[52] 4.167s passed
jmodjmod data()[53] 4.287s passed
jmodDivisible data()[54] 4.164s passed
jmodDivisibleRep data()[55] 4.189s passed
jdivAddMultDenom data()[56] 4.426s passed
jmodAltZero data()[57] 4.143s passed
jmodAddMultDenomZero data()[58] 4.190s passed
polyDiv_zero data()[59] 4.247s passed
cancel_gtPos data()[5] 4.604s passed
polyMod_ltdivDenom data()[60] 4.027s passed
bsum_empty data()[61] 3.962s passed
bsum_induction_upper data()[62] 4.136s passed
bsum_induction_lower data()[63] 4.203s passed
bsum_num_of_bounds data()[64] 4.140s passed
bsum_num_of_bounds2 data()[65] 4.250s passed
bsum_induction_upper2 data()[66] 4.232s passed
bsum_induction_upper_concrete data()[67] 4.294s passed
bsum_induction_upper_concrete_2 data()[68] 4.178s passed
bsum_induction_upper2_concrete data()[69] 4.145s passed
cancel_gtNeg data()[6] 4.349s passed
bsum_induction_lower_concrete data()[70] 4.134s passed
bsum_induction_lower2 data()[71] 4.054s passed
bsum_induction_lower2_concrete data()[72] 4.035s passed
bsum_positive data()[73] 4.238s passed
bsum_upper_bound data()[74] 4.236s passed
bsum_lower_bound data()[75] 4.307s passed
bsum_positive_lower_bound_element data()[76] 4.353s passed
bsum_sub_same_index data()[77] 4.241s passed
bsum_less_same_index data()[78] 4.230s passed
bsum_equal_except_one_index data()[79] 4.295s passed
moduloIntIsInInt data()[7] 4.335s passed
bsum_num_of_is_max data()[80] 4.154s passed
bsum_num_of_is_max2 data()[81] 4.146s passed
bsum_num_of_is_max3 data()[82] 4.077s passed
bsum_num_of_is_max4 data()[83] 4.260s passed
bsum_num_of_lt_max data()[84] 4.155s passed
bsum_num_of_lt_max2 data()[85] 4.148s passed
bsum_num_of_lt_max3 data()[86] 4.203s passed
bsum_num_of_lt_max4 data()[87] 4.096s passed
bsum_num_of_gt0 data()[88] 4.118s passed
bsum_num_of_gt0_alt data()[89] 4.260s passed
moduloLongIsInLong data()[8] 4.383s passed
bsum_add_concrete data()[90] 4.293s passed
bprod_all_positive data()[91] 4.053s passed
bprod_split data()[92] 4.146s passed
powConcrete0 data()[93] 4.183s passed
powConcrete1 data()[94] 4.240s passed
powSplitFactor data()[95] 4.039s passed
powAdd data()[96] 4.199s passed
powMono data()[97] 4.199s passed
powMonoConcrete data()[98] 4.209s passed
powMonoConcreteRight data()[99] 4.180s passed
moduloShortIsInShort data()[9] 4.246s passed

Standard output

800        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
838        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 16.88ms 
1136       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1168       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)

2402       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2405       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2407       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2407       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4986       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
12353      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 11.22s 
12451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
12504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.6ns 
12527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.24ms 
12535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
16501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
17778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
17819      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.82ms 
17834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
17834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 
17836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
21452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
22649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
22669      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
22671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
22671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
22673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
26110      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
27236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
27245      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
27251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
27252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 508.8ns 
27253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
30620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
31696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 564.9ns 
31699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
35011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
36198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
36298      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.68ms 
36300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
36301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.4ms 
36306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
39547      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40647      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.32ms 
40650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
40652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
43886      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44981      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.5ns 
44984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.6ns 
44987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
48320      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
49362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
49366      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.8ns 
49368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
49369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431ns 
49370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
52580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
53609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53612      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.3ns 
53615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53616      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 676.1ns 
53619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
56781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
57790      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
57793      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.5ns 
57796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
57797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.4ns 
57799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
61019      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62040      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.8ns 
62043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
62045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
65416      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
66467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
66570      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.4ms 
66572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
66572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
66578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
69761      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
70779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
70876      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.56ms 
70886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
70886      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
70888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
74071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
75091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
75376      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 274.53ms 
75379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
75379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
75380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
78630      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
79707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79715      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.37ms 
79720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271ns 
79721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82933      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
82934      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
83973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
83976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
83978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
83978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
83979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
87068      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
88091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
88150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.72ms 
88153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
88154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.5ns 
88155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
91331      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
92309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
92334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.66ms 
92338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
92338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.8ns 
92340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
95503      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
96519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
96539      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
96543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
96543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.9ns 
96545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99633      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
99633      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
100638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
100662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
100664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
100665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.1ns 
100666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
103929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
104896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
104918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.06ms 
104920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
104920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
104921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
108158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
109187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
109222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.79ms 
109224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
109225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.2ns 
109226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
112398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
113449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
113453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
113455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
113455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
113457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
116591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
117616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
117678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.93ms 
117683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
117683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.9ns 
117684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
120854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
121809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
121941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.86ms 
121945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
121945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.5ns 
121946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
125109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
126155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
126219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.18ms 
126221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
126221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
126222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
129263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
130315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
130326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.99ms 
130330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
130330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.9ns 
130331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
133546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
134523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
134544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.45ms 
134546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
134547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.4ns 
134550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
137789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
138826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
138842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
138844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
138844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
138845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
142034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
143027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
143038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
143040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
143040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
143041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
146235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
147190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
147200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
147203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
147203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.9ns 
147205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
150322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
151346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
151357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
151360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
151360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 
151361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
154541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
155546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
155550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
155552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
155552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
155553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
158652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
159664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
159680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
159683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
159683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.2ns 
159685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
162850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
163819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
163894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.87ms 
163897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
163897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.1ns 
163898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
167176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
168210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
168245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.05ms 
168248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
168248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.7ns 
168251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
171341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
172363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
172392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.72ms 
172395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
172395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.5ns 
172396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
175578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
176600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
176630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.06ms 
176633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
176633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392ns 
176636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
179852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
180900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
180927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.14ms 
180930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
180930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 
180932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
184028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
185108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
185176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.33ms 
185180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
185180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.6ns 
185183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
188372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
189403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
189407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
189408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
189408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
189409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
192581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
193619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
193626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
193628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
193628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
193629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
196704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
197716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
197728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 
197729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
197729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
197730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
200783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
201806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
201825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
201827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
201827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
201828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
204887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
205828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
205856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.69ms 
205859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
205859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301ns 
205861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
208996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
210014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
210025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
210028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
210028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
210029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
213167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
214193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
214198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
214200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
214200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.9ns 
214202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
217389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
218384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
218392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
218394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
218394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
218396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
221682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
222669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
222675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
222676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
222676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
222678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
225803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
226790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
226903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.75ms 
226906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
226907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.6ns 
226908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
230066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
231068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
231189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.06ms 
231192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
231192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.9ns 
231193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
234349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
235350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
235356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
235358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
235359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.4ns 
235360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
238540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
239593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
239642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.39ms 
239644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
239645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.2ns 
239646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
242745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
243761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
243806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.6ms 
243809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
243809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.8ns 
243811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
247010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
247991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
247996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
247998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
247998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
247999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
251187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
252200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
252421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 208.85ms 
252425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
252425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.3ns 
252427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
255554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
256551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
256566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.48ms 
256568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
256568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
256569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
259739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
260743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
260755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
260758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
260758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.9ns 
260759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
263965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
264979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
265003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.64ms 
265005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
265005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
265006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
268048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
269002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
269029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
269033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
269033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.6ns 
269034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
272028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
272988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
272993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
272995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
272995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.4ns 
272996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
276138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
277123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
277129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
277131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
277131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
277132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
280283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
281294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
281332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.83ms 
281334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
281334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
281335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
284428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
285444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
285469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 
285475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
285476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.3ns 
285477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
288696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
289701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
289723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ms 
289725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
289725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
289726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
292941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
293948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
293955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
293957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
293957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
293958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
297194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
298243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
298249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
298251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
298251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
298252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
301479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
302420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
302428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
302429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
302429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
302430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
305540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
306568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
306573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
306574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
306574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
306575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
309710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
310703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
310706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
310708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
310708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
310709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
313707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
314755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
314760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
314762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
314762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.6ns 
314763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
317837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
318792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
318795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
318797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
318797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
318798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
321904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
322958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
323033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.04ms 
323035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
323035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.4ns 
323037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
326173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
327192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
327269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.57ms 
327271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
327271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
327272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
330496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
331518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
331576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.98ms 
331578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
331578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
331579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
334824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
335850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
335929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.68ms 
335931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
335931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.6ns 
335932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
339091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
340122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
340170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.17ms 
340171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
340172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
340173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
343284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
344310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
344400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.79ms 
344402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
344402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.8ns 
344404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
347599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
348639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
348694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.02ms 
348696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
348696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
348698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
351817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
352817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
352849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.68ms 
352851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
352851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
352852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
355973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
356957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
356995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.75ms 
356997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
356997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
356998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
360087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
361043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
361072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.77ms 
361074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
361074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
361075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
364267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
365285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
365332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.38ms 
365334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
365334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.5ns 
365335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
368461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
369446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
369487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.34ms 
369489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
369490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.3ns 
369490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
372623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
373598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
373635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.41ms 
373636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
373637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
373638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
376754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
377803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
377838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.66ms 
377840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
377840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
377841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
380888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
381898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
381934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.3ms 
381936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
381936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
381937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
385046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
386015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
386052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.53ms 
386054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
386054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
386055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
389256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
390269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
390312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.92ms 
390314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
390314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
390315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
393543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
394594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
394605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
394607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
394607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
394608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
397648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
398630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
398658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.32ms 
398660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
398660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
398661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
401775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
402799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
402805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
402806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
402806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
402807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
405971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
406984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
406987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.9ns 
406989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
406989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
406990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
410204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
411223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
411227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
411228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
411228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
411229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
414303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
415256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
415266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
415268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
415268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
415269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
418436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
419456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
419465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
419467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
419467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
419468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
422639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
423646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
423664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
423667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
423667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
423668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
426839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
427869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
427874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
427875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
427875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
427876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
431016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
432050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
432053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.3ns 
432055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
432055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
432055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
435107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
436116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
436124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
436125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
436126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
436126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
439165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
440193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
440196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859ns 
440202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
440202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
440203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
443306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
444247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
444250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.9ns 
444251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
444251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
444252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
447302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
448320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
448323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820ns 
448324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
448324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
448325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
451443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
452475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
452480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
452482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
452482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
452483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
455676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
456677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
456690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
456692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
456692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
456693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
459839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
460906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
460911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
460913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
460913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
460914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
464076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
465101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
465112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
465114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
465114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
465115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
468262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
469257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
469263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
469264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
469264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
469265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
472362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
473319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
473345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.81ms 
473347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
473347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
473348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
476523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
477536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
477541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
477543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
477543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
477544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
480744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
481787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
481791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
481793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
481793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
481794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
485041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
486051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
486056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
486057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
486057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
486058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
489244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
490258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
490287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
490289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
490289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
490290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
493458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
494481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
494487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.1ns 
494489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
494489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
494490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
497659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
498658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
498718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.4ms 
498720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
498720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
498721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
501851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
502859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
502863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
502865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
502865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
502866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
506008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
506985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
507029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.48ms 
507031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
507031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
507032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
510178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
511185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
511215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.22ms 
511217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
511217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
511218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
514389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
515413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
515448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.73ms 
515450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
515450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
515451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
518572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
519585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
519588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822ns 
519590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
519590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
519591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
522722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
523729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
523739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
523741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
523741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
523742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
526870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
527882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
527886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
527889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
527889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.8ns 
527890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
531034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
532030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
532034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
532035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
532035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
532036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
535163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
536179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
536183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
536185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
536186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.9ns 
536187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
539316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
540311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
540315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
540317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
540317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
540318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
543426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
544428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
544432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
544433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
544433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
544434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
547590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
548582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
548596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.05ms 
548598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
548598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
548599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
551729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
552739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
552756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
552760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
552760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 
552761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
555853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
556887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
556903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.37ms 
556904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
556904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
556905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
560086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
561104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
561124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
561127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
561127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.5ns 
561128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
564289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
565319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
565325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
565327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
565327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
565328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
568490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
569515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
569523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
569525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
569525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
569525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
572623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
573644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
573647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
573649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
573649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
573650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
576784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
577794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
577798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
577800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
577800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
577801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
580944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
581952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
581955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
581957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
581957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
581958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
585175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
586214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
586230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.64ms 
586231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
586231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
586232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
589405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
590431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
590437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
590440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
590440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
590441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
593595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
594632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
594641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
594643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
594643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
594644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
597774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
598830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
598833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
598835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
598835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
598836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
602000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
603032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
603035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
603037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
603037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
603038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
606314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
607349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
607356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
607358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
607358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
607359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
610558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
611614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
611619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
611621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
611621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
611622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
614784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
615820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
615824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
615826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
615826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
615827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
618938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
619948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
619952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
619953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
619953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
619958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
623133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
624156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
624164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
624167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
624167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
624168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
627278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
628295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
628299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
628300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
628300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
628301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
631466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
632457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
632472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
632474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
632474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
632474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
635627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
636630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
636633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
636634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
636634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
636635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
639737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
640742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
640752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.72ms 
640754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
640754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
640755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
643871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
644852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
644855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
644857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
644857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
644857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
647976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
649020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
649024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
649025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
649025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
649026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
652163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
653194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
653200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
653202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
653202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
653203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
656340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
657365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
657369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
657372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
657372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.2ns 
657373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
660546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
661569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
661574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
661577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
661577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
661578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
664739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
665777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
665783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
665784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
665784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
665785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
668975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
670022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
670029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
670031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
670031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
670032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
673166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
674200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
674221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
674222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
674222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
674223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
677359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
678435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
678460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.58ms 
678462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
678462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
678464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
681640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
682651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
682665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
682666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
682667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
682667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
685812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
686929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
686946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 
686948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
686948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
686949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
690139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
691185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
691223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.8ms 
691225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
691225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
691226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
694421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
695458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
695496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.92ms 
695498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
695498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
695499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
698743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
699793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
699827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.41ms 
699829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
699829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
699830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
703039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
704079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
704103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
704105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
704105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
704106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
707317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
708364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
708410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.57ms 
708412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
708412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
708413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
711650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
712702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
712771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.77ms 
712772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
712772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns 
712773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
715982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
717031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
717092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.46ms 
717094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
717094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
717095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
720350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
721407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
721469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.71ms 
721471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
721471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
721472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
724729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
725781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
725848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.61ms 
725849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
725849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
725850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
729092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
730147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
730329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 174.17ms 
730331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
730332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
730332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
733571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
734628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
734644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.03ms 
734647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
734647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.7ns 
734648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
737860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
738903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
738916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
738918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
738918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
738919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
742115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
743145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
743153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
743154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
743154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
743155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
746347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
747409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
747436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.98ms 
747438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
747438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
747439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
750572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
751582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
751597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 
751599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
751599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
751600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
754762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
755804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
755808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
755812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
755812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
755813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
758992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
760029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
760055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
760056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
760056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
760057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
763209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
764235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
764259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
764261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
764261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
764262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
767464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
768484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
768512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.05ms 
768513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
768514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
768514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
771676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
772711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
772716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
772718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
772718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
772719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
775876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
776934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
776939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
776941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
776941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
776942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
780133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
781169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
781177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
781179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
781179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
781180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
784293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
785327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
785336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
785338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
785338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
785339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
788497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
789565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
789675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.42ms 
789676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
789677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
789677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
792828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
793879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
793922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.93ms 
793923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
793923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
793924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
797064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
798127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
798163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ms 
798165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
798165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
798166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
801319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
802335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
802338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.4ns 
802339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
802339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
802341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
805481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
806519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
806822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.54ms 
806825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
806825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.6ns 
806826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
809969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
811008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
811088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.36ms 
811090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
811090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
811091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
814225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
815264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
815267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.9ns 
815269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
815270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.3ns 
815271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
818388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
819441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
819443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.3ns 
819445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
819445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
819446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
822632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
822632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
823688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
823692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
823693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
823693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
823694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
826883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
827938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
827942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
827943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
827943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
827944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
831070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
832081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
832216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.72ms 
832219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
832219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.1ns 
832220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
835343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
836383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
836443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.98ms 
836444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
836444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
836453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
839667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
840712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
840714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.2ns 
840751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
840802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
840839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
840848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
840861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
840865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
840867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
840871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
840877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
840881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
840887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
840889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
841184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
841185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
841186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
841188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
841189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
841377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
841379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
841380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
841383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
841384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
841385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
841602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
841604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
841605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
841606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
841607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
841609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
841758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
841760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
841761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
841762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
841763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
841764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
841772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
841773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
841774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
841777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
841778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
841779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
841787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
841788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
841789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
841790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
841791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
841792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
841974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
841977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
841978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
842117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
842120     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)'' 
842123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
842124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
842125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
842127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
842128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
842128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
842137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
842139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
842140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
842141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
842142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
842331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
842336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
842338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
842339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
842340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
842341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
842342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
842498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
842500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
842501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
842503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
842504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
842505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
842506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
842508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
842637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
842639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
842756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
842762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
842769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
842771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
842772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
842774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
842775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
842775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
842776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
842778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
842789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
842795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
842923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
842925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
842926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
842927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
842928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
842929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
842930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
842931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
843002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
843009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
843130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
843133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
843135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
843137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
843138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
843139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
843323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
843330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
843332     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)'' 
843334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
843335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
843336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
843337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
843338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
843349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
843351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
843353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
843360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
843482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
843485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
843487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
843488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
843489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
843490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
843627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
843629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
843631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
843633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
843634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
843634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
843635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
843637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
843747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
843749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
843848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
843849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
843850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
843900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
843906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
843911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
844081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
844083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
844084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
844085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
844098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
844208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
848902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
848903     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)'' 
848910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
848911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
848912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
848913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
848914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
848925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
848928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
848930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
848931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
848932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
849061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
849066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
849067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
849068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
849068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
849069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
849070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
849280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
849281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
849282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
849283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
849284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
849284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
849285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
849286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
849397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
849399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
849500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
849506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
849511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
849513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
849514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
849515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
849528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
849635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
849637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
849637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
849638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
849742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
849755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
849756     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)'' 
849758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
849759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
849760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
849760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
849761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
849777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
849779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
849780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
849781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
849781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
849904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
849906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
849907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
849907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
849908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
850038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
850045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
850047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
850049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
850049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
850050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
850051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
850185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
850187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
850187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
850189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
850189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
850190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
850193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
850196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
850197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
850198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
850199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
850200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
850200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
850201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
850202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
850327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
850328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
850336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
850445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
850558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
850560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
850561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
850562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
850563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
850563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
850564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
850564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
850565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
850685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
850694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
850820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
850822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
850822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
850824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
850824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
850824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
850825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
850826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
850833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
850833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
850949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
850957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
850964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
851104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
851105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
851106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
851107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
851108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
851108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
851109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
851109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
851185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
851186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
851187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
851188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
851189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
851196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
851204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
851368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
851551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
851552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
851553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
851554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
851784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
851907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
851908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
856060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
856065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
856066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
856067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
856068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
856219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
856220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
856222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
856222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
856223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
856359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
860488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
864740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
864745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
864746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
864747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
864748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
864897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
864898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
864900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
864901     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)' ...' 
864903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
866471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
866471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
866472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
869609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
869609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
870664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
870666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
870666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
870678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
870693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
870697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
870700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
870701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
870709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
870711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
870716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
870719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
870720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
870732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
870735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
870735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
870801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
870805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
870807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
870808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
870809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
870914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
870915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
870918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
870919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
870920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
870927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
870928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
870928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
870930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
870931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
870932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
871050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
871051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
871052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
871053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
871055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
871056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
871181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
871182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
871183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
871184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
871185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
871186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
871187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
871187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
871188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
871189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
871190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
871190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
871191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
871191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
871192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
871193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
871193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
871195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
871196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
871199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
871252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
871254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
871328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
871330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
871332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
871334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
871335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
871336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
871420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
871423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
871425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
871427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
871428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
871429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
871430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
871500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
871504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
871508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
871577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
871650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
871651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.3ns 
871652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
874848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
875963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
876007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.45ms