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

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

tests
0

failures
0

ignored
14m43.41s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.154s passed
powPositiveConcrete data()[101] 4.192s passed
powGeq1Concrete data()[102] 4.211s passed
pow2InIntLower data()[103] 4.184s passed
pow2InIntUpper data()[104] 4.259s passed
logSelfConcrete data()[105] 4.204s passed
log1Concrete data()[106] 4.204s passed
logProduct data()[107] 4.197s passed
logTimesBaseConcrete data()[108] 4.121s passed
logProdIdentity data()[109] 4.135s passed
moduloByteIsInByte data()[10] 4.358s passed
logProdIdentityConcrete data()[110] 4.132s passed
logPowIdentity data()[111] 4.152s passed
logPowIdentityConcrete data()[112] 4.117s passed
logPositive data()[113] 4.150s passed
logPositiveConcrete data()[114] 4.175s passed
logMono data()[115] 4.184s passed
logMonoConcrete data()[116] 4.172s passed
powLogLess data()[117] 4.159s passed
powLogMore2 data()[118] 4.004s passed
logLessThanPow data()[119] 4.016s passed
moduloCharIsInChar data()[11] 4.389s passed
logLessThanPowConcrete data()[120] 3.996s passed
logSqueeze data()[121] 3.999s passed
ifthenelse_equals data()[122] 3.980s passed
ifthenelse_equals_1 data()[123] 4.051s passed
ifthenelse_equals_2 data()[124] 4.126s passed
disjointWithSingleton1 data()[125] 4.062s passed
disjointWithSingleton2 data()[126] 4.181s passed
disjointArrayRanges data()[127] 4.464s passed
disjointArrayRangeAllFields1 data()[128] 4.246s passed
disjointArrayRangeAllFields2 data()[129] 4.152s passed
div_unique1 data()[12] 4.539s passed
seqSelfDefinition data()[130] 4.222s passed
seqOutsideValue data()[131] 4.158s passed
castedGetAny data()[132] 4.221s passed
seqGetAlphaCast data()[133] 4.191s passed
getOfSeqSingleton data()[134] 4.143s passed
getOfSeqSingletonConcrete data()[135] 4.020s passed
getOfSeqConcat data()[136] 4.048s passed
getOfSeqSub data()[137] 4.131s passed
getOfSeqReverse data()[138] 4.149s passed
lenOfSeqEmpty data()[139] 4.190s passed
div_unique2 data()[13] 4.344s passed
lenOfSeqSingleton data()[140] 4.378s passed
lenOfSeqConcat data()[141] 4.440s passed
lenOfSeqSub data()[142] 4.282s passed
lenOfSeqReverse data()[143] 4.331s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.282s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.363s passed
getOfSeqSingletonEQ data()[146] 4.336s passed
getOfSeqConcatEQ data()[147] 4.384s passed
getOfSeqSubEQ data()[148] 4.334s passed
getOfSeqReverseEQ data()[149] 4.365s passed
div_exists data()[14] 4.564s passed
lenOfSeqEmptyEQ data()[150] 4.377s passed
lenOfSeqSingletonEQ data()[151] 4.433s passed
lenOfSeqConcatEQ data()[152] 4.343s passed
lenOfSeqSubEQ data()[153] 4.318s passed
lenOfSeqReverseEQ data()[154] 4.325s passed
getOfSeqDefEQ data()[155] 4.307s passed
lenOfSeqDefEQ data()[156] 4.410s passed
seqConcatWithSeqEmpty1 data()[157] 4.371s passed
seqConcatWithSeqEmpty2 data()[158] 4.368s passed
seqReverseOfSeqEmpty data()[159] 4.344s passed
div_one data()[15] 4.326s passed
subSeqComplete data()[160] 4.453s passed
subSeqTailR data()[161] 4.421s passed
subSeqTailL data()[162] 4.376s passed
subSeqTailEQR data()[163] 4.334s passed
subSeqTailEQL data()[164] 4.471s passed
seqDef_split data()[165] 4.482s passed
seqDef_induction_upper data()[166] 4.408s passed
seqDef_induction_upper_concrete data()[167] 4.505s passed
seqDef_induction_lower data()[168] 4.609s passed
seqDef_induction_lower_concrete data()[169] 4.490s passed
jdiv_one data()[16] 4.300s passed
seqDef_split_in_three data()[170] 4.678s passed
seqDef_empty data()[171] 4.562s passed
seqDef_one_summand data()[172] 4.357s passed
seqDef_lower_equals_upper data()[173] 4.486s passed
seqDefOfSeq data()[174] 4.434s passed
seqSelfDefinitionEQ2 data()[175] 4.520s passed
indexOfSeqSingleton data()[176] 4.446s passed
indexOfSeqConcatFirst data()[177] 4.431s passed
indexOfSeqConcatSecond data()[178] 4.482s passed
indexOfSeqSub data()[179] 4.457s passed
div_zero data()[17] 4.374s passed
lenOfArray2seq data()[180] 4.385s passed
getAnyOfArray2seq data()[181] 4.492s passed
getOfArray2seq data()[182] 4.361s passed
getAnyOfNPermInv data()[183] 4.425s passed
seqNPermRange data()[184] 4.539s passed
seqPermTrans data()[185] 4.428s passed
seqPermRefl data()[186] 4.511s passed
seqPermSplit data()[187] 4.488s passed
seqNPermRight data()[188] 4.816s passed
seqPermFromSwap data()[189] 4.455s passed
divResZero1 data()[18] 4.464s passed
seqPermTransAlt0 data()[190] 4.350s passed
seqPermTransAlt1 data()[191] 4.433s passed
seqPermTransAlt2 data()[192] 4.442s passed
seqPermTransAlt3 data()[193] 4.391s passed
seqPermForall data()[194] 4.487s passed
seqPermExists data()[195] 4.481s passed
schiffl_lemma_2 data()[196] 31.682s passed
schiffl_thm_1 data()[197] 5.844s passed
eqSameSeq data()[198] 4.569s passed
divResZero2 data()[19] 4.380s passed
eqTermCut data()[1] 5.206s passed
divResOne1 data()[20] 4.321s passed
divResOne2 data()[21] 4.356s passed
div_cancel1 data()[22] 4.312s passed
div_cancel2 data()[23] 4.272s passed
divAddMultDenom data()[24] 4.348s passed
divMinus data()[25] 4.528s passed
divMinusDenom data()[26] 4.415s passed
divLeastDPos data()[27] 4.297s passed
divLeastDNeg data()[28] 4.423s passed
divGreatestDPos data()[29] 4.399s passed
equivAllRight data()[2] 4.896s passed
divGreatestDNeg data()[30] 4.326s passed
divIncreasingPos data()[31] 4.433s passed
divIncreasingNeg data()[32] 4.344s passed
jdiv_zero data()[33] 4.338s passed
jdivPulloutMinusNum data()[34] 4.286s passed
jdivPulloutMinusDenom data()[35] 4.497s passed
jdiv_uniquePosPos data()[36] 4.262s passed
jdiv_uniquePosNeg data()[37] 4.295s passed
jdiv_uniqueNegPos data()[38] 4.229s passed
jdiv_uniqueNegNeg data()[39] 4.267s passed
irrflConcrete1 data()[3] 4.733s passed
jdivMultDenom1 data()[40] 4.256s passed
jdivMultDenom2 data()[41] 4.218s passed
mod_geZero data()[42] 4.247s passed
mod_lessDenom data()[43] 4.239s passed
jmod_NumPos data()[44] 4.231s passed
jmod_NumNeg data()[45] 4.179s passed
jmod_geZero data()[46] 4.201s passed
jmodNumZero data()[47] 4.207s passed
jmod_pulloutminusNum data()[48] 4.242s passed
jmod_pulloutminusDenom data()[49] 4.185s passed
irrflConcrete2 data()[4] 4.625s passed
jmodUnique1 data()[50] 4.320s passed
jmodUnique2 data()[51] 4.318s passed
intDivRem data()[52] 4.233s passed
jmodjmod data()[53] 4.223s passed
jmodDivisible data()[54] 4.130s passed
jmodDivisibleRep data()[55] 4.108s passed
jdivAddMultDenom data()[56] 4.419s passed
jmodAltZero data()[57] 4.228s passed
jmodAddMultDenomZero data()[58] 4.227s passed
polyDiv_zero data()[59] 4.236s passed
cancel_gtPos data()[5] 4.684s passed
polyMod_ltdivDenom data()[60] 4.396s passed
bsum_empty data()[61] 4.251s passed
bsum_induction_upper data()[62] 4.263s passed
bsum_induction_lower data()[63] 4.292s passed
bsum_num_of_bounds data()[64] 4.435s passed
bsum_num_of_bounds2 data()[65] 4.284s passed
bsum_induction_upper2 data()[66] 4.403s passed
bsum_induction_upper_concrete data()[67] 4.288s passed
bsum_induction_upper_concrete_2 data()[68] 4.240s passed
bsum_induction_upper2_concrete data()[69] 4.234s passed
cancel_gtNeg data()[6] 4.481s passed
bsum_induction_lower_concrete data()[70] 4.202s passed
bsum_induction_lower2 data()[71] 4.229s passed
bsum_induction_lower2_concrete data()[72] 4.152s passed
bsum_positive data()[73] 4.260s passed
bsum_upper_bound data()[74] 4.253s passed
bsum_lower_bound data()[75] 4.358s passed
bsum_positive_lower_bound_element data()[76] 4.329s passed
bsum_sub_same_index data()[77] 4.181s passed
bsum_less_same_index data()[78] 4.300s passed
bsum_equal_except_one_index data()[79] 4.259s passed
moduloIntIsInInt data()[7] 4.397s passed
bsum_num_of_is_max data()[80] 4.202s passed
bsum_num_of_is_max2 data()[81] 4.253s passed
bsum_num_of_is_max3 data()[82] 4.211s passed
bsum_num_of_is_max4 data()[83] 4.222s passed
bsum_num_of_lt_max data()[84] 4.253s passed
bsum_num_of_lt_max2 data()[85] 4.251s passed
bsum_num_of_lt_max3 data()[86] 4.247s passed
bsum_num_of_lt_max4 data()[87] 4.219s passed
bsum_num_of_gt0 data()[88] 4.180s passed
bsum_num_of_gt0_alt data()[89] 4.255s passed
moduloLongIsInLong data()[8] 4.371s passed
bsum_add_concrete data()[90] 4.200s passed
bprod_all_positive data()[91] 4.258s passed
bprod_split data()[92] 4.185s passed
powConcrete0 data()[93] 4.243s passed
powConcrete1 data()[94] 4.225s passed
powSplitFactor data()[95] 4.208s passed
powAdd data()[96] 4.152s passed
powMono data()[97] 4.270s passed
powMonoConcrete data()[98] 4.229s passed
powMonoConcreteRight data()[99] 4.211s passed
moduloShortIsInShort data()[9] 4.374s passed

Standard output

470        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
522        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 20.46ms 
853        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
870        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)

2227       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2230       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2234       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2234       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4212       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.61s 
11555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11605      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.1ns 
11626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11627      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 818.21ns 
11633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 
15567      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16820      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.47ms 
16833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16833      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214ns 
16835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 
20545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21723      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
21730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.2ns 
21733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
25295      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
26463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.2ns 
26465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
29928      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31083      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
31090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.03ms 
31094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
34597      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.01ms 
35776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 686.2ns 
35779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
39129      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40253      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
40257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40258      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.5ns 
40259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
43579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44652      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830ns 
44655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.9ns 
44657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
47948      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
49018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
49023      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 682.9ns 
49026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
49026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 528.4ns 
49028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
52305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
53387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53393      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
53402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53403      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 569.6ns 
53405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
56707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
57753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
57757      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.5ns 
57760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
57760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.1ns 
57762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
61056      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62145      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666.7ns 
62148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.5ns 
62150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
65452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
66555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
66678      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.01ms 
66690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
66690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.9ns 
66692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
69927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
70984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
71029      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.79ms 
71033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
71033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.8ns 
71035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
74296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
75341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
75593      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 240.56ms 
75597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
75597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400ns 
75599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
78906      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
79912      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79920      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
79922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.8ns 
79924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83173      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
83174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
84215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
84220      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
84224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
84224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.2ns 
84226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87496      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
87496      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
88537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
88596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.83ms 
88599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
88599      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.7ns 
88601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
91959      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
93029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
93059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.74ms 
93062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
93062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.3ns 
93064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96353      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
96353      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
97417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
97439      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.09ms 
97442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
97443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.7ns 
97444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
100699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
101730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
101760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.01ms 
101764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
101764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.91ns 
101766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
105061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
106096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
106117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.34ms 
106119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
106119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
106120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
109359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
110392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
110429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.51ms 
110430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
110431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 
110432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
113654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
114697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
114701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
114703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
114703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.8ns 
114704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
117947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
118978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
119049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.72ms 
119051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
119052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.8ns 
119054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
122357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
123439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
123572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.16ms 
123579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
123579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 
123581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
126912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
127914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
127992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.99ms 
127994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
127994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
127995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
131264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
132277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
132289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.02ms 
132291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
132291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.7ns 
132292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
135616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
136690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
136711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.33ms 
136735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
136736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 736.3ns 
136739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
140067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
141101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
141120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.81ms 
141124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
141124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns 
141125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
144413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
145436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
145448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.31ms 
145450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
145450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.4ns 
145451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
148755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
149863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
149880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
149885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
149887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.04ms 
149889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
153194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
154215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
154226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
154227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
154228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
154229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
157509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
158559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
158564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
158565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
158565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
158566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
161814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
162824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
162850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.36ms 
162852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
162852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.8ns 
162854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
166153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
167224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
167341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.23ms 
167358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
167359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.3ns 
167367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
170558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
171583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
171618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.3ms 
171620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
171620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.6ns 
171621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
174853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
175882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
175913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.98ms 
175914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
175915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
175916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
179093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
180110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
180142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.98ms 
180143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
180144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
180145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
183349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
184375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
184408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.33ms 
184410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
184411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
184412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
187555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
188594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
188663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.5ms 
188668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
188669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.8ns 
188670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
191878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
192880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
192883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
192885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
192885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
192886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
196098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
197124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
197130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
197132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
197132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
197133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
200343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
201358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
201369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
201371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
201371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.3ns 
201373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
204550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
205588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
205600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ms 
205602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
205602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
205603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
208734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
209746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
209779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.3ms 
209780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
209780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
209782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
212955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
213967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
213980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
213984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
213984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
213985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
217164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
218184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
218188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
218191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
218191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.9ns 
218196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
221402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
222426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
222431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
222433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
222433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
222434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
225601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
226610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
226616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
226618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
226618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
226619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
229782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
230780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
230935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.56ms 
230939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
230939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
230941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
234099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
235114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
235254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.4ms 
235257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
235257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.6ns 
235258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
238470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
239482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
239487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
239490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
239490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.7ns 
239491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
242631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
243651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
243711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.99ms 
243712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
243713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.3ns 
243713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
246820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
247786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.52ms 
247843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
247844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
250926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
251945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
251949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
251950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
251950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
251952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
255111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
256121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
256368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 232.55ms 
256371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
256371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.1ns 
256372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
259555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
260580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
260596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
260598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
260598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
260599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
263767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
264809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
264823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
264825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
264825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
264826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
268015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
269031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
269059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.86ms 
269061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
269061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
269062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
272371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
273434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
273453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
273456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
273457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
273457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
276698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
277701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
277706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
277707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
277708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
277708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
280936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
281959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
281969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
281971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
281971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
281972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
285170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
286221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
286261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.03ms 
286263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
286263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
286264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
289665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
290672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
290696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.35ms 
290698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
290698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 
290699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
293916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
294953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
294980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
294982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
294982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.8ns 
294983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
298291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
299379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
299383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
299386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
299386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
299387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
302611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
303665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
303671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
303672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
303672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
303674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
306867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
307902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
307911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
307913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
307913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
307914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
311123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
312141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
312145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
312148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
312148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.5ns 
312149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
315315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
316344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
316347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.31ns 
316348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
316348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
316349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
319549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
320570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
320576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
320577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
320578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
320578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
323683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
324725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
324728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
324730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
324730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
324731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
327885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
328893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
328988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.09ms 
328991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
328991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
328994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
332175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
333169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
333241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.62ms 
333243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
333243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
333244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
336521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
337541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
337598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.11ms 
337601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
337601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.9ns 
337602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
340813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
341822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
341927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.17ms 
341931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
341931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.9ns 
341932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
345075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
346060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
346110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.63ms 
346111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
346111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
346112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
349261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
350313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
350408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.37ms 
350412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
350413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238ns 
350414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
353622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
354620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
354668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.92ms 
354670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
354671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
354671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
357843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
358839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
358870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.96ms 
358872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
358872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
358873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
362061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
363083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
363123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.8ms 
363125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
363125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
363126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
366302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
367303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
367334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.53ms 
367335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
367335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
367336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
370495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
371511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
371556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.31ms 
371558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
371558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
371559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
374759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
375767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
375809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.11ms 
375811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
375811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
375812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
378990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
379984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
380059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71ms 
380062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
380063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.4ns 
380065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
383249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
384266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
384307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.89ms 
384309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
384309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
384310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
387484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
388492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
388526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.05ms 
388527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
388527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
388528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
391681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
392666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
392706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms 
392708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
392708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
392709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
395876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
396916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
396962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.35ms 
396963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
396963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
396964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
400121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
401150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
401161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.91ms 
401162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
401163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.7ns 
401163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
404376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
405390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
405419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.66ms 
405420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
405420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
405421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
408581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
409599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
409604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
409605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
409605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
409606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
412814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
413844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
413847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.51ns 
413848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
413848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
413850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
417048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
418069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
418072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
418074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
418074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
418075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
421246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
422269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
422281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
422282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
422282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
422283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
425420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
426423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
426432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
426434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
426434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
426435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
429619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
430683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
430702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
430705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
430705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.1ns 
430707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
433893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
434926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
434931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
434933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
434933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
434934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
438118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
439139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
439142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.91ns 
439143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
439144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
439144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
442286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
443290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
443297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
443298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
443298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
443299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
446479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
447485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
447488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.71ns 
447489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
447490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
447490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
450664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
451697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
451699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.71ns 
451701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
451701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
451702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
454890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
455881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
455883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865ns 
455885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
455885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
455886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
459126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
460138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
460143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
460144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
460144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
460145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
463322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
464333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
464346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.53ms 
464348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
464348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
464349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
467522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
468542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
468550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
468553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
468553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.1ns 
468559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
471744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
472737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
472747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
472748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
472748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
472749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
475859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
476863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
476869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
476870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
476870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
476871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
479981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
480979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
481003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
481005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
481005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
481006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
484137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
485131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
485135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
485137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
485137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
485138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
488290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
489279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
489287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
489290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
489290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.3ns 
489291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
492394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
493399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
493404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
493406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
493406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
493407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
496544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
497524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
497554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms 
497556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
497556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.5ns 
497557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
500721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
501723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
501728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.31ns 
501730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
501730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
501731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
504853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
505855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
505913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.67ms 
505915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
505915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
505916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
509066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
510081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
510085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
510087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
510087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
510087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
513201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
514212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
514244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.5ms 
514246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
514246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
514247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
517253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
518220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
518248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
518250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
518250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
518251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
521265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
522230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
522264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.43ms 
522265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
522265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
522266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
525273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
526257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
526260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.41ns 
526262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
526262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.7ns 
526263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
529279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
530252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
530259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
530261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
530261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
530262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
533275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
534235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
534239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
534240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
534240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
534241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
537266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
538287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
538290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 991.81ns 
538292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
538292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
538293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
541415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
542414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
542417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
542418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
542418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
542419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
545422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
546472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
546478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
546483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
546483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
546484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
549627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
550658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
550662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
550663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
550663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
550664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
554052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
555110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
555126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
555128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
555128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
555128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
558343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
559355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
559371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
559374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
559374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
559375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
562504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
563507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
563525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.91ms 
563526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
563526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
563527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
566667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
567722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
567747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.06ms 
567748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
567748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
567749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
570900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
571898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
571904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
571905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
571905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
571906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
575050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
576116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
576126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
576127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
576127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
576128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
579297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
580314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
580317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.91ns 
580319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
580319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.7ns 
580320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
583454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
584456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
584459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
584461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
584462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
584462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
587474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
588476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
588479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
588480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
588481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
588481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
591496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
592512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
592527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
592529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
592529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
592529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
595636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
596654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
596659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
596660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
596660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
596661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
599776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
600798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
600807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
600809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
600809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
600810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
603977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
604995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
604998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.41ns 
604999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
604999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
605000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
608290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
609373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
609375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.31ns 
609377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
609377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
609378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
612715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
613808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
613815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
613816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
613816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
613817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
617044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
618093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
618097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
618101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
618101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.4ns 
618102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
621379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
622426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
622430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
622432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
622432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
622432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
625671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
626707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
626712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
626713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
626714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
626714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
630016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
631067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
631075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
631076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
631076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
631077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
634361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
635407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
635411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
635413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
635413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
635414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
638715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
639778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
639795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
639798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
639798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.3ns 
639799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
643068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
644126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
644129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
644131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
644131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
644132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
647420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
648475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
648493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.89ms 
648496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
648496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.1ns 
648497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
651823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
652868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
652871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
652873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
652873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
652874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
656223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
657301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
657304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
657306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
657306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
657307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
660549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
661640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
661647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
661648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
661648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
661649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
664913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
665961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
665965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
665967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
665967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
665968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
669219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
670285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
670290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
670292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
670292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
670293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
673530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
674592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
674597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
674599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
674599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
674600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
677911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
678996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
679007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.38ms 
679010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
679010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
679011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
682293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
683357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
683378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.37ms 
683380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
683380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
683380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
686677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
687722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
687746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.11ms 
687747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
687747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
687748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
691018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
692075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
692090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
692092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
692092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
692093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
695449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
696527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
696543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
696545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
696545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
696546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
699855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
700916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
700964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.45ms 
700966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
700966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
700967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
704254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
705305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
705340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.16ms 
705341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
705341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
705342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
708585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
709639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
709674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.32ms 
709675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
709675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
709676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
713021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
714123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
714144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
714147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
714147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.3ns 
714148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
717503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
718582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
718627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.01ms 
718629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
718629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
718630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
721898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
722956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
723035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.98ms 
723037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
723037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
723038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
726388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
727476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
727540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.83ms 
727542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
727543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
727544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
731016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
732084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
732149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.05ms 
732150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
732150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
732151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
735470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
736570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
736639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.91ms 
736641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
736641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
736642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
740006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
741099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
741317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 208.46ms 
741319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
741319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
741320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
744768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
745868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
745879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
745881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
745881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
745882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
749140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
750224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
750236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
750237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
750238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
750238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
753631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
754715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
754723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
754724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
754724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
754725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
758031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
759124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
759155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.1ms 
759158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
759158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
759159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
762574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
763657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
763675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.47ms 
763677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
763678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.5ns 
763679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
766985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
768118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
768122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
768123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
768124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
768124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
771437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
772526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
772553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
772555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
772555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
772555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
775914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
777005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
777035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.71ms 
777037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
777038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 
777039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
780385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
781461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
781492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.34ms 
781494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
781495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.8ns 
781496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
784790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
785872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
785877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
785879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
785879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
785880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
789308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
790363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
790369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
790371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
790371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
790372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
793607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
794723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
794730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
794731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
794731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
794732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
798064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
799146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
799155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
799157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
799157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.5ns 
799158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
802468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
803563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
803693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.52ms 
803695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
803696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.7ns 
803696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
807018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
808080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
808122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.46ms 
808125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
808125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272ns 
808126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
811495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
812599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
812633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.32ms 
812635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
812635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
812636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
816040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
817118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
817121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.6ns 
817122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
817123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
817124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
820513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
821588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
821935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297.26ms 
821939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
821939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295ns 
821941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
825197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
826278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
826392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.95ms 
826394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
826394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
826395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
829678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
830740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
830743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 431.5ns 
830745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
830745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.9ns 
830746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
834086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
835173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
835176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.5ns 
835177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
835177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
835178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
838538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
839615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
839618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.1ns 
839619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
839619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
839620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
842947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
842948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
844004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
844008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
844010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
844010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
844011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
847276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
847276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
848368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
848495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 124.47ms 
848498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
848498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.6ns 
848499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
851797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
852910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
852976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.99ms 
852978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
852979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
852982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
856356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
857471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
857474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
857513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
857657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
857690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
857700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
857714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
857718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
857720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
857723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
857734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
857738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
857746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
857748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
858103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
858105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
858107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
858108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
858109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
858293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
858295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
858298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
858301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
858303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
858305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
858512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
858516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
858519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
858520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
858521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
858526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
858682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
858685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
858687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
858688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
858689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
858691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
858700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
858702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
858702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
858706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
858708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
858710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
858722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
858724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
858726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
858727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
858730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
858731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
858889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
858890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
858893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
859037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
859039     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)'' 
859043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
859044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
859046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
859048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
859049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
859053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
859060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
859062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
859064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
859064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
859066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
859202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
859207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
859209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
859211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
859213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
859215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
859218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
859379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
859382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
859383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
859385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
859388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
859389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
859392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
859395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
859516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
859518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
859638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
859645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
859656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
859658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
859659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
859660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
859661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
859661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
859661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
859663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
859673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
859685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
859806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
859809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
859812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
859813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
859814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
859814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
859815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
859817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
859881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
859889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
860024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
860027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
860030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
860032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
860034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
860040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
860217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
860223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
860227     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)'' 
860230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
860232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
860233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
860234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
860235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
860250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
860263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
860265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
860266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
860394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
860396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
860396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
860397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
860398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
860398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
860536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
860538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
860540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
860542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
860543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
860544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
860545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
860546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
860660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
860664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
860767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
860768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
860769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
860776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
860782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
860789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
861003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
861004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
861005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
861006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
861019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
861134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
866372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
866373     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)'' 
866379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
866380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
866381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
866382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
866382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
866393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
866395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
866397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
866399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
866400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
866532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
866538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
866540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
866541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
866541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
866542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
866543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
866679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
866681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
866683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
866685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
866686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
866687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
866687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
866689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
866802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
866804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
866912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
866924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
866930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
866932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
866932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
866933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
866947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
867058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
867060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
867061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
867062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
867159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
867171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
867173     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)'' 
867175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
867176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
867176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
867177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
867177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
867193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
867195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
867196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
867196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
867197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
867321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
867322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
867324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
867324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
867325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
867447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
867453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
867455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
867455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
867456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
867457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
867458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
867597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
867599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
867599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
867601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
867602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
867603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
867603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
867605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
867606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
867606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
867608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
867609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
867609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
867609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
867611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
867741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
867743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
867754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
867867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
867981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
867983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
867985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
867986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
867987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
867987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
867988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
867988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
867989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
868108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
868119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
868309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
868310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
868311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
868313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
868313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
868314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
868314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
868315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
868322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
868323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
868430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
868437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
868445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
868581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
868583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
868583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
868585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
868585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
868585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
868586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
868587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
868661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
868663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
868663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
868664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
868666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
868673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
868683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
868841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
868958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
868959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
868960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
868961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
869186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
869302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
869303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
873629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
873635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
873636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
873636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
873637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
873794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
873796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
873797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
873798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
873799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
873946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
878262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
882764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
882769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
882770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
882771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
882772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
882976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
882978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
882979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
882980     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)' ...' 
882982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
884659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
884660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
884661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
888438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
888438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
889560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
889562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
889563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
889574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
889590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
889593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
889596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
889597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
889603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
889605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
889610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
889613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
889615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
889628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
889631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
889632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
889691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
889692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
889693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
889694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
889695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
889786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
889788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
889790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
889791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
889792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
889798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
889799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
889800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
889801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
889802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
889803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
889917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
889918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
889919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
889921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
889923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
889924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
890053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
890054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
890055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
890056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
890057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
890058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
890059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
890059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
890060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
890061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
890062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
890062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
890063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
890064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
890064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
890065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
890066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
890067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
890068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
890072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
890119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
890121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
890196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
890198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
890200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
890201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
890202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
890203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
890267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
890271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
890273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
890275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
890277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
890278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
890279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
890344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
890348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
890353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
890425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
890504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
890504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 
890505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
893908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
893908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
895026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
895071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.56ms