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

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

tests
0

failures
0

ignored
11m29.66s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.345s passed
powPositiveConcrete data()[101] 3.308s passed
powGeq1Concrete data()[102] 3.309s passed
pow2InIntLower data()[103] 3.323s passed
pow2InIntUpper data()[104] 3.337s passed
logSelfConcrete data()[105] 3.340s passed
log1Concrete data()[106] 3.332s passed
logProduct data()[107] 3.351s passed
logTimesBaseConcrete data()[108] 3.338s passed
logProdIdentity data()[109] 3.364s passed
moduloByteIsInByte data()[10] 3.485s passed
logProdIdentityConcrete data()[110] 3.338s passed
logPowIdentity data()[111] 3.344s passed
logPowIdentityConcrete data()[112] 3.350s passed
logPositive data()[113] 3.342s passed
logPositiveConcrete data()[114] 3.340s passed
logMono data()[115] 3.368s passed
logMonoConcrete data()[116] 3.340s passed
powLogLess data()[117] 3.356s passed
powLogMore2 data()[118] 3.350s passed
logLessThanPow data()[119] 3.349s passed
moduloCharIsInChar data()[11] 3.456s passed
logLessThanPowConcrete data()[120] 3.341s passed
logSqueeze data()[121] 3.325s passed
ifthenelse_equals data()[122] 3.319s passed
ifthenelse_equals_1 data()[123] 3.335s passed
ifthenelse_equals_2 data()[124] 3.330s passed
disjointWithSingleton1 data()[125] 3.344s passed
disjointWithSingleton2 data()[126] 3.334s passed
disjointArrayRanges data()[127] 3.354s passed
disjointArrayRangeAllFields1 data()[128] 3.363s passed
disjointArrayRangeAllFields2 data()[129] 3.355s passed
div_unique1 data()[12] 3.494s passed
seqSelfDefinition data()[130] 3.360s passed
seqOutsideValue data()[131] 3.355s passed
castedGetAny data()[132] 3.354s passed
seqGetAlphaCast data()[133] 3.373s passed
getOfSeqSingleton data()[134] 3.339s passed
getOfSeqSingletonConcrete data()[135] 3.345s passed
getOfSeqConcat data()[136] 3.346s passed
getOfSeqSub data()[137] 3.352s passed
getOfSeqReverse data()[138] 3.344s passed
lenOfSeqEmpty data()[139] 3.340s passed
div_unique2 data()[13] 3.473s passed
lenOfSeqSingleton data()[140] 3.350s passed
lenOfSeqConcat data()[141] 3.339s passed
lenOfSeqSub data()[142] 3.373s passed
lenOfSeqReverse data()[143] 3.343s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.341s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.387s passed
getOfSeqSingletonEQ data()[146] 3.355s passed
getOfSeqConcatEQ data()[147] 3.392s passed
getOfSeqSubEQ data()[148] 3.341s passed
getOfSeqReverseEQ data()[149] 3.353s passed
div_exists data()[14] 3.585s passed
lenOfSeqEmptyEQ data()[150] 3.348s passed
lenOfSeqSingletonEQ data()[151] 3.339s passed
lenOfSeqConcatEQ data()[152] 3.373s passed
lenOfSeqSubEQ data()[153] 3.347s passed
lenOfSeqReverseEQ data()[154] 3.335s passed
getOfSeqDefEQ data()[155] 3.336s passed
lenOfSeqDefEQ data()[156] 3.358s passed
seqConcatWithSeqEmpty1 data()[157] 3.347s passed
seqConcatWithSeqEmpty2 data()[158] 3.360s passed
seqReverseOfSeqEmpty data()[159] 3.377s passed
div_one data()[15] 3.416s passed
subSeqComplete data()[160] 3.359s passed
subSeqTailR data()[161] 3.363s passed
subSeqTailL data()[162] 3.382s passed
subSeqTailEQR data()[163] 3.357s passed
subSeqTailEQL data()[164] 3.342s passed
seqDef_split data()[165] 3.386s passed
seqDef_induction_upper data()[166] 3.398s passed
seqDef_induction_upper_concrete data()[167] 3.413s passed
seqDef_induction_lower data()[168] 3.400s passed
seqDef_induction_lower_concrete data()[169] 3.382s passed
jdiv_one data()[16] 3.431s passed
seqDef_split_in_three data()[170] 3.489s passed
seqDef_empty data()[171] 3.355s passed
seqDef_one_summand data()[172] 3.366s passed
seqDef_lower_equals_upper data()[173] 3.343s passed
seqDefOfSeq data()[174] 3.383s passed
seqSelfDefinitionEQ2 data()[175] 3.367s passed
indexOfSeqSingleton data()[176] 3.364s passed
indexOfSeqConcatFirst data()[177] 3.351s passed
indexOfSeqConcatSecond data()[178] 3.376s passed
indexOfSeqSub data()[179] 3.350s passed
div_zero data()[17] 3.424s passed
lenOfArray2seq data()[180] 3.353s passed
getAnyOfArray2seq data()[181] 3.342s passed
getOfArray2seq data()[182] 3.356s passed
getAnyOfNPermInv data()[183] 3.344s passed
seqNPermRange data()[184] 3.420s passed
seqPermTrans data()[185] 3.408s passed
seqPermRefl data()[186] 3.369s passed
seqPermSplit data()[187] 3.376s passed
seqNPermRight data()[188] 3.593s passed
seqPermFromSwap data()[189] 3.411s passed
divResZero1 data()[18] 3.412s passed
seqPermTransAlt0 data()[190] 3.357s passed
seqPermTransAlt1 data()[191] 3.359s passed
seqPermTransAlt2 data()[192] 3.330s passed
seqPermTransAlt3 data()[193] 3.358s passed
seqPermForall data()[194] 3.463s passed
seqPermExists data()[195] 3.445s passed
schiffl_lemma_2 data()[196] 21.918s passed
schiffl_thm_1 data()[197] 4.064s passed
eqSameSeq data()[198] 3.437s passed
divResZero2 data()[19] 3.416s passed
eqTermCut data()[1] 4.169s passed
divResOne1 data()[20] 3.388s passed
divResOne2 data()[21] 3.515s passed
div_cancel1 data()[22] 3.461s passed
div_cancel2 data()[23] 3.388s passed
divAddMultDenom data()[24] 3.410s passed
divMinus data()[25] 3.414s passed
divMinusDenom data()[26] 3.393s passed
divLeastDPos data()[27] 3.382s passed
divLeastDNeg data()[28] 3.400s passed
divGreatestDPos data()[29] 3.381s passed
equivAllRight data()[2] 3.790s passed
divGreatestDNeg data()[30] 3.371s passed
divIncreasingPos data()[31] 3.364s passed
divIncreasingNeg data()[32] 3.407s passed
jdiv_zero data()[33] 3.397s passed
jdivPulloutMinusNum data()[34] 3.389s passed
jdivPulloutMinusDenom data()[35] 3.430s passed
jdiv_uniquePosPos data()[36] 3.376s passed
jdiv_uniquePosNeg data()[37] 3.380s passed
jdiv_uniqueNegPos data()[38] 3.394s passed
jdiv_uniqueNegNeg data()[39] 3.409s passed
irrflConcrete1 data()[3] 3.628s passed
jdivMultDenom1 data()[40] 3.432s passed
jdivMultDenom2 data()[41] 3.378s passed
mod_geZero data()[42] 3.371s passed
mod_lessDenom data()[43] 3.378s passed
jmod_NumPos data()[44] 3.353s passed
jmod_NumNeg data()[45] 3.389s passed
jmod_geZero data()[46] 3.368s passed
jmodNumZero data()[47] 3.379s passed
jmod_pulloutminusNum data()[48] 3.362s passed
jmod_pulloutminusDenom data()[49] 3.342s passed
irrflConcrete2 data()[4] 3.603s passed
jmodUnique1 data()[50] 3.444s passed
jmodUnique2 data()[51] 3.421s passed
intDivRem data()[52] 3.335s passed
jmodjmod data()[53] 3.384s passed
jmodDivisible data()[54] 3.381s passed
jmodDivisibleRep data()[55] 3.354s passed
jdivAddMultDenom data()[56] 3.515s passed
jmodAltZero data()[57] 3.373s passed
jmodAddMultDenomZero data()[58] 3.368s passed
polyDiv_zero data()[59] 3.341s passed
cancel_gtPos data()[5] 3.558s passed
polyMod_ltdivDenom data()[60] 3.359s passed
bsum_empty data()[61] 3.336s passed
bsum_induction_upper data()[62] 3.339s passed
bsum_induction_lower data()[63] 3.367s passed
bsum_num_of_bounds data()[64] 3.359s passed
bsum_num_of_bounds2 data()[65] 3.364s passed
bsum_induction_upper2 data()[66] 3.342s passed
bsum_induction_upper_concrete data()[67] 3.345s passed
bsum_induction_upper_concrete_2 data()[68] 3.333s passed
bsum_induction_upper2_concrete data()[69] 3.348s passed
cancel_gtNeg data()[6] 3.504s passed
bsum_induction_lower_concrete data()[70] 3.360s passed
bsum_induction_lower2 data()[71] 3.361s passed
bsum_induction_lower2_concrete data()[72] 3.337s passed
bsum_positive data()[73] 3.446s passed
bsum_upper_bound data()[74] 3.432s passed
bsum_lower_bound data()[75] 3.396s passed
bsum_positive_lower_bound_element data()[76] 3.402s passed
bsum_sub_same_index data()[77] 3.407s passed
bsum_less_same_index data()[78] 3.391s passed
bsum_equal_except_one_index data()[79] 3.381s passed
moduloIntIsInInt data()[7] 3.501s passed
bsum_num_of_is_max data()[80] 3.384s passed
bsum_num_of_is_max2 data()[81] 3.403s passed
bsum_num_of_is_max3 data()[82] 3.370s passed
bsum_num_of_is_max4 data()[83] 3.368s passed
bsum_num_of_lt_max data()[84] 3.382s passed
bsum_num_of_lt_max2 data()[85] 3.393s passed
bsum_num_of_lt_max3 data()[86] 3.382s passed
bsum_num_of_lt_max4 data()[87] 3.355s passed
bsum_num_of_gt0 data()[88] 3.384s passed
bsum_num_of_gt0_alt data()[89] 3.361s passed
moduloLongIsInLong data()[8] 3.467s passed
bsum_add_concrete data()[90] 3.350s passed
bprod_all_positive data()[91] 3.370s passed
bprod_split data()[92] 3.338s passed
powConcrete0 data()[93] 3.331s passed
powConcrete1 data()[94] 3.337s passed
powSplitFactor data()[95] 3.343s passed
powAdd data()[96] 3.336s passed
powMono data()[97] 3.342s passed
powMonoConcrete data()[98] 3.326s passed
powMonoConcreteRight data()[99] 3.327s passed
moduloShortIsInShort data()[9] 3.491s passed

Standard output

334        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
388        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 20.87ms 
680        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701        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)

1677       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1679       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1684       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1684       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3291       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8870       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.19s 
8950       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8988       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.5ns 
9003       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9005       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.02ms 
9011       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
12089      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13162      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.72ms 
13177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 
13180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
16037      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16965      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.05ms 
16968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.1ns 
16970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
19676      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20591      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
20597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.6ns 
20599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
23316      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
24191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24197      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
24200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.2ns 
24201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
26824      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.02ms 
27759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 695.8ns 
27761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30371      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
30372      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31225      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.8ms 
31262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.8ns 
31263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
33893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.5ns 
34764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.2ms 
34767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
37373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
38229      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.7ns 
38231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
38231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.2ns 
38232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
40834      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
41722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.5ns 
41723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
44341      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
45202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
45205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.8ns 
45207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
45207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.6ns 
45208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
47813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.8ns 
48663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
48664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51244      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
51245      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
52115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
52155      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.57ms 
52157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
52157      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
52160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54750      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
54751      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.34ms 
55630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.6ns 
55631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58201      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
58202      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
59043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
59213      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.63ms 
59217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
59217      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.7ns 
59218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
61781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62630      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
62631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
62632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
65189      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
66058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
66061      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
66063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
66063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
66064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
68614      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
69446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.62ms 
69487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141ns 
69488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
72046      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72897      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.04ms 
72899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72899      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.1ns 
72900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75442      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
75442      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
76279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
76309      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.04ms 
76315      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
76315      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168ns 
76316      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78850      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
78850      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79701      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
79703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.3ns 
79704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
82256      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
83168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
83215      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.8ms 
83229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
83229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.3ns 
83230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
85811      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86686      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.39ms 
86690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.7ns 
86692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
89234      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
90072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
90076      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
90079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
90079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.9ns 
90080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
92598      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
93441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
93486      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.77ms 
93488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
93488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
93489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
96009      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96900      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.45ms 
96903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.7ns 
96904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99416      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
99417      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
100246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
100292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.63ms 
100294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
100294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
100295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
102832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.13ms 
103682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.9ns 
103683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
106222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
107061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
107075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ms 
107077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
107078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.5ns 
107079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
109615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
110458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.9ns 
110460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
112982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
113829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
113830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
116354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
117182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
117190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
117193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
117193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.6ns 
117194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
119751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
120600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322ns 
120601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
123155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
123996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
123997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
126543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
127372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
127383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.87ms 
127386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
127386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314ns 
127387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
129917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.85ms 
130817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.4ns 
130818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
133341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
134174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
134191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.96ms 
134193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
134193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
134194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
136720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
137573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
137574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
140106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.03ms 
140967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
140968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
143520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
144358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
144374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
144376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
144376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
144377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
146932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.86ms 
147809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.4ns 
147810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
150347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
151181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
151184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
151185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
151186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
151186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
153721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
154550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
154555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
154556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
154557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
154557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
157080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
157934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns 
157935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
160455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
161279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
161287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
161288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
161288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
161289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
163819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
164678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 555.4ns 
164679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
167206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
168034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
168043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
168044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
168045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
168045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
170595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
171417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
171421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
171425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
171425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.4ns 
171426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
173975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
174780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
174784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
174785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
174785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
174786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
177323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
178122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
178126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
178127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
178127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
178128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
180674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
181475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
181569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.99ms 
181573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
181573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
181574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
184107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
184992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.48ms 
184994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
184994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.1ns 
184995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
187521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
188324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
188327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
188329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
188329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
188330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
190860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
191660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
191710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.17ms 
191714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
191719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.4ms 
191721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
194265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
195063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
195091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.44ms 
195093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
195093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
195094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
197643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
198443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
198446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
198451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
198452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.6ns 
198453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
200996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
201804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
201963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.91ms 
201967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
201967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.93ns 
201968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
204526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
205326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
205337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
205339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
205339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
205340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
207890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
208697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
208705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ms 
208707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
208707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
208708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
211229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
212029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
212046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.39ms 
212048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
212048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
212049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
214589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
215391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
215404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
215406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
215406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
215407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
217934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
218738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
218742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
218743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
218743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
218744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
221270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
222076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
222081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
222082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
222082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
222083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
224621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
225423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
225447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.67ms 
225449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
225449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
225450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
227980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
228790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
228806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
228808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
228808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
228809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
231352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
232155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
232170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
232172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
232172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
232173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
234696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
235507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
235512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
235514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
235514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
235514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
238046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
238853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
238857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
238859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
238859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
238859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
241386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
242185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
242191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
242192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
242192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
242193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
244735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
245535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
245538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
245540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
245540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
245540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
248089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
248896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
248898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.51ns 
248900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
248900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
248901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
251448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
252255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
252259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
252260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
252260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
252261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
254791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
255594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
255597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
255598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
255598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
255599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
258134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
258964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
259042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.76ms 
259045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
259045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.11ns 
259046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
261606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
262434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
262474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.07ms 
262487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
262488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
262488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
265017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
265849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
265882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.24ms 
265884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
265884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
265885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
268408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
269238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
269284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.11ms 
269286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
269286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
269287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
271838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
272661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
272691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.48ms 
272693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
272693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
272694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
275204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
276031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
276082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.48ms 
276084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
276084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
276085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
278596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
279429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
279463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.58ms 
279465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
279465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
279466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
281998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
282825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
282847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ms 
282850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
282850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 
282851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
285398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
286226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
286250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.81ms 
286252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
286252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
286253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
288771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
289600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
289620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.61ms 
289622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
289622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
289623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
292136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
292961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
292988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.26ms 
292989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
292989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
292990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
295514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
296343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
296370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.23ms 
296371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
296371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
296372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
298900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
299736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
299763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.4ms 
299764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
299764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
299765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
302288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
303120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
303145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.98ms 
303146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
303146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
303147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
305647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
306478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
306500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.79ms 
306501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
306501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
306502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
309027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
309857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
309884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.25ms 
309885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
309885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
309886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
312393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
313220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
313245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.13ms 
313247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
313247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
313248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
315756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
316587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
316595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
316596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
316597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
316597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
319118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
319947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
319965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.67ms 
319967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
319967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
319968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
322473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
323299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
323303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
323305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
323305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.9ns 
323306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
325805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
326632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
326635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.51ns 
326636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
326636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
326637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
329140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
329969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
329971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.4ns 
329974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
329974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
329975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
332486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
333309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
333316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
333317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
333318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
333318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
335815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
336645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
336652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
336654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
336654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.4ns 
336655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
339151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
339982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
339994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.29ms 
339996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
339996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
339997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
342493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
343317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
343321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
343322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
343322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
343323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
345822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
346645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
346647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.61ns 
346649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
346649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
346650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
349157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
349986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
349992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
349993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
349993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
349994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
352474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
353298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
353300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.71ns 
353301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
353302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
353302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
355785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
356607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
356609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.1ns 
356611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
356611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
356611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
359103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
359929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
359932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.61ns 
359934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
359934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.7ns 
359935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
362439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
363265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
363269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
363270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
363270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
363271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
365775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
366600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
366609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
366614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
366614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
366615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
369114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
369940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
369944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
369945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
369945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
369946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
372456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
373288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
373295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
373297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
373297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
373297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
375805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
376629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
376633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
376635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
376635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
376635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
379144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
379972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
379997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ms 
379999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
380000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.7ns 
380000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
382510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
383332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
383335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
383337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
383337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
383337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
385845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
386676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
386679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
386680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
386680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
386681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
389191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
390025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
390030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
390031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
390031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
390032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
392529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
393354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
393371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
393373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
393373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
393374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
395878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
396705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
396710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.5ns 
396713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
396713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.6ns 
396714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
399220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
400041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
400079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.53ms 
400081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
400081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
400081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
402586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
403414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
403420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
403421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
403421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
403423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
405928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
406752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
406775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.38ms 
406776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
406777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
406777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
409278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
410105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
410126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.78ms 
410127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
410127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
410128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
412624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
413450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
413474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.79ms 
413476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
413476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
413477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
415985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
416812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
416815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 658.9ns 
416817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
416818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 
416818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
419314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
420134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
420140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
420141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
420141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
420142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
422628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
423456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
423459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
423460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
423461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
423461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
425967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
426792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
426795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 902ns 
426796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
426796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
426797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
429296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
430122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
430124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.91ns 
430126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
430126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
430127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
432658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
433465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
433468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
433470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
433470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
433470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
435989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
436798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
436802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
436805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
436805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
436805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
439338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
440147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
440157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
440159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
440159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
440159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
442696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
443508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
443521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
443522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
443522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
443523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
446056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
446863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
446875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
446877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
446877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
446877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
449411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
450222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
450235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
450236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
450236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
450237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
452766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
453580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
453590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
453592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
453592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
453593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
456122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
456937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
456945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.28ms 
456946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
456946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
456947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
459472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
460313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
460317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.59ns 
460319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
460319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212ns 
460320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
462816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
463653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
463656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
463658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
463658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
463659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
466162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
466999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
467001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 918.1ns 
467003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
467003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
467004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
469499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
470336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
470347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
470349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
470349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
470350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
472854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
473694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
473699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
473701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
473701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
473702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
476200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
477035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
477043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
477045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
477045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.1ns 
477046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
479545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
480381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
480383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.4ns 
480384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
480384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
480385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
482916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
483730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
483733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.71ns 
483734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
483734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
483735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
486254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
487068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
487072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
487074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
487074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
487075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
489598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
490443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
490446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
490447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
490447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
490448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
492944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
493786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
493789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
493790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
493790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
493791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
496290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
497127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
497130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
497131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
497131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
497132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
499669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
500510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
500516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
500517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
500517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
500518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
503053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
503868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
503871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
503873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
503873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
503874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
506404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
507222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
507263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.91ms 
507265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
507265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
507265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
509759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
510601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
510604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.6ns 
510605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
510605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
510606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
513111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
513949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
513957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
513958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
513958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
513959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
516467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
517303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
517305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 991.4ns 
517306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
517307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
517307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
519832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
520642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
520644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830ns 
520646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
520646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
520646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
523175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
524012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
524018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
524019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
524019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
524020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
526523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
527361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
527365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
527366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
527366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
527367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
529859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
530696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
530700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
530701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
530701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
530702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
533217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
534031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
534035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
534038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
534038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
534038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
536554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
537390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
537395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
537396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
537396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
537397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
539891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
540727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
540742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
540743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
540743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
540744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
543267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
544086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
544101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.64ms 
544103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
544103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
544103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
546629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
547468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
547479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
547480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
547480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
547481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
549988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
550826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
550837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.01ms 
550839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
550839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
550840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
553340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
554174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
554200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.36ms 
554201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
554201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
554202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
556724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
557557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
557582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.94ms 
557584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
557584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
557585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
560079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
560915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
560939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
560941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
560941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
560942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
563454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
564266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
564281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms 
564282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
564282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
564283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
566797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
567637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
567668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.51ms 
567669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
567669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
567670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
570175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
571017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
571065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.56ms 
571067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
571067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
571068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
573601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
574436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
574477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.38ms 
574480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
574480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 
574481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
576996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
577833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
577878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.54ms 
577879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
577879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
577880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
580404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
581216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
581260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.7ms 
581262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
581262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
581263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
583790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
584628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
584749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.98ms 
584751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
584751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
584752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
587281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
588096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
588104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
588106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
588106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
588107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
590624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
591462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
591470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
591472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
591472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
591472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
593967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
594808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
594813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
594815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
594815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
594816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
597338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
598178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
598197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms 
598198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
598198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
598199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
600712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
601552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
601563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.98ms 
601564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
601564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
601565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
604088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
604924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
604927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
604929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
604929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
604929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
607425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
608261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
608278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ms 
608280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
608280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
608280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
610802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
611637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
611654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
611655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
611656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
611656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
614150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
614985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
615004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.66ms 
615006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
615006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
615006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
617514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
618354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
618357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
618359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
618359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
618360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
620851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
621695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
621699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
621701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
621701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
621702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
624214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
625048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
625055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
625056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
625057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
625057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
627578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
628392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
628399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
628400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
628401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
628401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
630918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
631751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
631819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.58ms 
631821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
631821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
631822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
634359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
635199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
635227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.27ms 
635229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
635229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.7ns 
635230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
637735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
638573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
638596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.21ms 
638597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
638597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
638598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
641125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
641971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
641973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.7ns 
641974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
641974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
641976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
644506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
645325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
645565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.34ms 
645568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
645568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.1ns 
645569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
648080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
648922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
648976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.78ms 
648978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
648979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.8ns 
648979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
651494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
652331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
652333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 393.2ns 
652335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
652335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
652335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
654852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
655690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
655692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 393.6ns 
655693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
655693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
655694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
658182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
659020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
659022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.9ns 
659023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
659023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
659024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
661538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
662378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
662381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.4ns 
662382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
662382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
662383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
664892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
665727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
665843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.5ms 
665846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
665846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns 
665847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
668389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
669232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
669288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.45ms 
669289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
669289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
669291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
671826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
672674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
672676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 
672702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
672756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
672777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
672786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
672795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
672800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
672802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
672805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
672809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
672812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
672816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
672820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
673042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
673044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
673045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
673046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
673047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
673188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
673190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
673193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
673195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
673196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
673197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
673338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
673342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
673343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
673344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
673345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
673349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
673476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
673478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
673480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
673480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
673481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
673482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
673495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
673496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
673497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
673499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
673501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
673502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
673510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
673511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
673512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
673513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
673514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
673515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
673621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
673623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
673625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
673729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
673731     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)'' 
673735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
673736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
673737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
673739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
673740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
673742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
673749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
673751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
673752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
673753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
673754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
673862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
673866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
673868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
673869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
673870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
673871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
673873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
673990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
673992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
673994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
673996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
673997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
673998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
673999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
674001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
674089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
674091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
674171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
674174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
674179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
674182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
674183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
674185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
674188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
674188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
674189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
674190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
674197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
674202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
674283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
674285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
674286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
674288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
674289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
674290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
674290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
674291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
674335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
674340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
674418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
674420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
674422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
674424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
674425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
674426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
674576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
674580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
674582     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)'' 
674584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
674586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
674586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
674587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
674588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
674595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
674600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
674602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
674603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
674690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
674691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
674693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
674695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
674696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
674697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
674791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
674793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
674794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
674795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
674796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
674796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
674797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
674798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
674870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
674872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
674939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
674940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
674941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
674944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
674948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
674952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
675064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
675065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
675066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
675067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
675077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
675154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
678596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
678597     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)'' 
678602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
678603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
678604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
678605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
678606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
678613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
678615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
678616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
678617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
678617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
678707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
678711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
678713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
678714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
678714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
678715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
678716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
678807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
678809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
678810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
678811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
678811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
678813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
678814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
678815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
678891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
678893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
679017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
679022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
679027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
679028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
679029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
679030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
679041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
679123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
679124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
679127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
679130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
679215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
679227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
679227     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)'' 
679230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
679231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
679232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
679232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
679233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
679243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
679245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
679246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
679246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
679247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
679338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
679340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
679341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
679341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
679342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
679437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
679441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
679442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
679443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
679443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
679444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
679444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
679542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
679543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
679544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
679545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
679545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
679546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
679546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
679547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
679548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
679549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
679550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
679550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
679551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
679551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
679552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
679637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
679638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
679644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
679720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
679798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
679800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
679801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
679802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
679802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
679803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
679803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
679804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
679804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
679888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
679894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
679982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
679983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
679984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
679985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
679986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
679986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
679987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
679988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
679993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
679994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
680072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
680078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
680083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
680181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
680183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
680183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
680185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
680185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
680186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
680186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
680187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
680241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
680242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
680243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
680244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
680245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
680251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
680256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
680372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
680460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
680461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
680462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
680463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
680628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
680715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
680717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
683694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
683699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
683700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
683701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
683702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
683814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
683815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
683816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
683817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
683817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
683922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
686863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
689955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
689959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
689960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
689961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
689962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
690072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
690074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
690075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
690076     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)' ...' 
690077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
691208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
691208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
691209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
693810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
694678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
694679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
694680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
694688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
694699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
694701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
694703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
694703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
694708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
694709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
694712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
694715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
694716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
694725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
694727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
694727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
694769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
694770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
694771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
694771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
694772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
694827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
694827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
694829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
694830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
694830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
694834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
694834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
694835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
694836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
694837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
694837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
694901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
694902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
694902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
694904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
694904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
694905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
694970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
694971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
694972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
694972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
694973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
694974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
694975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
694975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
694976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
694977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
694977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
694978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
694978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
694979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
694979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
694980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
694980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
694982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
694982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
694985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
695013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
695015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
695059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
695061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
695063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
695064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
695065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
695065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
695106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
695108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
695110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
695111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
695113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
695113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
695114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
695157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
695160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
695163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
695216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
695273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
695273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 
695274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
697810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
698675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
698707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.76ms