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

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

tests
0

failures
0

ignored
13m1.86s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.780s passed
powPositiveConcrete data()[101] 3.775s passed
powGeq1Concrete data()[102] 3.794s passed
pow2InIntLower data()[103] 3.764s passed
pow2InIntUpper data()[104] 3.779s passed
logSelfConcrete data()[105] 3.777s passed
log1Concrete data()[106] 3.748s passed
logProduct data()[107] 3.796s passed
logTimesBaseConcrete data()[108] 3.754s passed
logProdIdentity data()[109] 3.792s passed
moduloByteIsInByte data()[10] 3.902s passed
logProdIdentityConcrete data()[110] 3.768s passed
logPowIdentity data()[111] 3.796s passed
logPowIdentityConcrete data()[112] 3.769s passed
logPositive data()[113] 3.777s passed
logPositiveConcrete data()[114] 3.809s passed
logMono data()[115] 3.857s passed
logMonoConcrete data()[116] 3.811s passed
powLogLess data()[117] 3.851s passed
powLogMore2 data()[118] 3.955s passed
logLessThanPow data()[119] 3.873s passed
moduloCharIsInChar data()[11] 3.840s passed
logLessThanPowConcrete data()[120] 3.978s passed
logSqueeze data()[121] 3.834s passed
ifthenelse_equals data()[122] 3.822s passed
ifthenelse_equals_1 data()[123] 3.836s passed
ifthenelse_equals_2 data()[124] 3.866s passed
disjointWithSingleton1 data()[125] 3.843s passed
disjointWithSingleton2 data()[126] 3.813s passed
disjointArrayRanges data()[127] 3.817s passed
disjointArrayRangeAllFields1 data()[128] 3.837s passed
disjointArrayRangeAllFields2 data()[129] 3.823s passed
div_unique1 data()[12] 4.097s passed
seqSelfDefinition data()[130] 3.834s passed
seqOutsideValue data()[131] 3.816s passed
castedGetAny data()[132] 3.814s passed
seqGetAlphaCast data()[133] 3.878s passed
getOfSeqSingleton data()[134] 3.820s passed
getOfSeqSingletonConcrete data()[135] 3.812s passed
getOfSeqConcat data()[136] 3.829s passed
getOfSeqSub data()[137] 3.825s passed
getOfSeqReverse data()[138] 3.960s passed
lenOfSeqEmpty data()[139] 3.809s passed
div_unique2 data()[13] 3.850s passed
lenOfSeqSingleton data()[140] 3.789s passed
lenOfSeqConcat data()[141] 3.788s passed
lenOfSeqSub data()[142] 3.798s passed
lenOfSeqReverse data()[143] 4.001s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.789s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.806s passed
getOfSeqSingletonEQ data()[146] 3.808s passed
getOfSeqConcatEQ data()[147] 3.811s passed
getOfSeqSubEQ data()[148] 3.809s passed
getOfSeqReverseEQ data()[149] 3.777s passed
div_exists data()[14] 4.154s passed
lenOfSeqEmptyEQ data()[150] 3.763s passed
lenOfSeqSingletonEQ data()[151] 3.836s passed
lenOfSeqConcatEQ data()[152] 3.796s passed
lenOfSeqSubEQ data()[153] 3.796s passed
lenOfSeqReverseEQ data()[154] 3.814s passed
getOfSeqDefEQ data()[155] 3.769s passed
lenOfSeqDefEQ data()[156] 3.764s passed
seqConcatWithSeqEmpty1 data()[157] 3.772s passed
seqConcatWithSeqEmpty2 data()[158] 3.784s passed
seqReverseOfSeqEmpty data()[159] 3.796s passed
div_one data()[15] 3.879s passed
subSeqComplete data()[160] 3.770s passed
subSeqTailR data()[161] 3.781s passed
subSeqTailL data()[162] 3.781s passed
subSeqTailEQR data()[163] 3.821s passed
subSeqTailEQL data()[164] 3.778s passed
seqDef_split data()[165] 3.823s passed
seqDef_induction_upper data()[166] 3.897s passed
seqDef_induction_upper_concrete data()[167] 3.860s passed
seqDef_induction_lower data()[168] 3.802s passed
seqDef_induction_lower_concrete data()[169] 3.861s passed
jdiv_one data()[16] 3.838s passed
seqDef_split_in_three data()[170] 3.929s passed
seqDef_empty data()[171] 3.809s passed
seqDef_one_summand data()[172] 3.788s passed
seqDef_lower_equals_upper data()[173] 3.786s passed
seqDefOfSeq data()[174] 3.816s passed
seqSelfDefinitionEQ2 data()[175] 3.769s passed
indexOfSeqSingleton data()[176] 3.744s passed
indexOfSeqConcatFirst data()[177] 3.787s passed
indexOfSeqConcatSecond data()[178] 3.754s passed
indexOfSeqSub data()[179] 3.800s passed
div_zero data()[17] 3.844s passed
lenOfArray2seq data()[180] 3.765s passed
getAnyOfArray2seq data()[181] 3.779s passed
getOfArray2seq data()[182] 3.769s passed
getAnyOfNPermInv data()[183] 3.780s passed
seqNPermRange data()[184] 3.846s passed
seqPermTrans data()[185] 3.835s passed
seqPermRefl data()[186] 3.859s passed
seqPermSplit data()[187] 3.872s passed
seqNPermRight data()[188] 3.993s passed
seqPermFromSwap data()[189] 3.870s passed
divResZero1 data()[18] 3.852s passed
seqPermTransAlt0 data()[190] 3.755s passed
seqPermTransAlt1 data()[191] 3.790s passed
seqPermTransAlt2 data()[192] 3.775s passed
seqPermTransAlt3 data()[193] 3.747s passed
seqPermForall data()[194] 3.890s passed
seqPermExists data()[195] 3.826s passed
schiffl_lemma_2 data()[196] 26.578s passed
schiffl_thm_1 data()[197] 4.637s passed
eqSameSeq data()[198] 3.838s passed
divResZero2 data()[19] 3.848s passed
eqTermCut data()[1] 4.492s passed
divResOne1 data()[20] 3.840s passed
divResOne2 data()[21] 3.841s passed
div_cancel1 data()[22] 3.846s passed
div_cancel2 data()[23] 3.808s passed
divAddMultDenom data()[24] 3.870s passed
divMinus data()[25] 4.113s passed
divMinusDenom data()[26] 3.880s passed
divLeastDPos data()[27] 3.849s passed
divLeastDNeg data()[28] 3.894s passed
divGreatestDPos data()[29] 3.920s passed
equivAllRight data()[2] 4.247s passed
divGreatestDNeg data()[30] 3.839s passed
divIncreasingPos data()[31] 3.795s passed
divIncreasingNeg data()[32] 3.789s passed
jdiv_zero data()[33] 3.813s passed
jdivPulloutMinusNum data()[34] 3.773s passed
jdivPulloutMinusDenom data()[35] 3.863s passed
jdiv_uniquePosPos data()[36] 3.872s passed
jdiv_uniquePosNeg data()[37] 3.837s passed
jdiv_uniqueNegPos data()[38] 3.781s passed
jdiv_uniqueNegNeg data()[39] 3.793s passed
irrflConcrete1 data()[3] 4.150s passed
jdivMultDenom1 data()[40] 3.878s passed
jdivMultDenom2 data()[41] 3.860s passed
mod_geZero data()[42] 3.869s passed
mod_lessDenom data()[43] 3.825s passed
jmod_NumPos data()[44] 3.803s passed
jmod_NumNeg data()[45] 3.837s passed
jmod_geZero data()[46] 3.794s passed
jmodNumZero data()[47] 3.864s passed
jmod_pulloutminusNum data()[48] 3.787s passed
jmod_pulloutminusDenom data()[49] 3.769s passed
irrflConcrete2 data()[4] 3.990s passed
jmodUnique1 data()[50] 3.908s passed
jmodUnique2 data()[51] 3.852s passed
intDivRem data()[52] 3.786s passed
jmodjmod data()[53] 3.822s passed
jmodDivisible data()[54] 3.787s passed
jmodDivisibleRep data()[55] 3.776s passed
jdivAddMultDenom data()[56] 3.948s passed
jmodAltZero data()[57] 3.804s passed
jmodAddMultDenomZero data()[58] 3.794s passed
polyDiv_zero data()[59] 3.856s passed
cancel_gtPos data()[5] 3.931s passed
polyMod_ltdivDenom data()[60] 3.784s passed
bsum_empty data()[61] 3.736s passed
bsum_induction_upper data()[62] 3.734s passed
bsum_induction_lower data()[63] 3.791s passed
bsum_num_of_bounds data()[64] 3.800s passed
bsum_num_of_bounds2 data()[65] 3.790s passed
bsum_induction_upper2 data()[66] 3.773s passed
bsum_induction_upper_concrete data()[67] 3.809s passed
bsum_induction_upper_concrete_2 data()[68] 3.766s passed
bsum_induction_upper2_concrete data()[69] 3.760s passed
cancel_gtNeg data()[6] 3.892s passed
bsum_induction_lower_concrete data()[70] 3.765s passed
bsum_induction_lower2 data()[71] 3.836s passed
bsum_induction_lower2_concrete data()[72] 3.772s passed
bsum_positive data()[73] 3.844s passed
bsum_upper_bound data()[74] 3.832s passed
bsum_lower_bound data()[75] 3.798s passed
bsum_positive_lower_bound_element data()[76] 3.805s passed
bsum_sub_same_index data()[77] 3.845s passed
bsum_less_same_index data()[78] 3.796s passed
bsum_equal_except_one_index data()[79] 3.787s passed
moduloIntIsInInt data()[7] 3.918s passed
bsum_num_of_is_max data()[80] 3.769s passed
bsum_num_of_is_max2 data()[81] 3.782s passed
bsum_num_of_is_max3 data()[82] 3.779s passed
bsum_num_of_is_max4 data()[83] 3.784s passed
bsum_num_of_lt_max data()[84] 3.777s passed
bsum_num_of_lt_max2 data()[85] 3.789s passed
bsum_num_of_lt_max3 data()[86] 3.802s passed
bsum_num_of_lt_max4 data()[87] 3.770s passed
bsum_num_of_gt0 data()[88] 3.788s passed
bsum_num_of_gt0_alt data()[89] 3.841s passed
moduloLongIsInLong data()[8] 3.890s passed
bsum_add_concrete data()[90] 3.775s passed
bprod_all_positive data()[91] 3.900s passed
bprod_split data()[92] 3.731s passed
powConcrete0 data()[93] 3.756s passed
powConcrete1 data()[94] 3.755s passed
powSplitFactor data()[95] 3.771s passed
powAdd data()[96] 3.749s passed
powMono data()[97] 3.760s passed
powMonoConcrete data()[98] 3.760s passed
powMonoConcreteRight data()[99] 3.754s passed
moduloShortIsInShort data()[9] 3.877s passed

Standard output

666        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
697        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.51ms 
961        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
981        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)

2030       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2033       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2037       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2038       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3549       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.28s 
10320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10362      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.6ns 
10380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10382      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.89ms 
10387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
13807      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.36ms 
14873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 
14875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
17958      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.75ms 
19121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425ns 
19123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
22164      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23268      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
23272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.8ns 
23274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26260      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
26260      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27260      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
27263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.7ns 
27265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
30175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31143      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.07ms 
31195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 625.71ns 
31198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
34100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35085      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.86ms 
35089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.1ns 
35090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
38012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.01ns 
39006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns 
39007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
41896      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
42890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
42894      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.81ns 
42897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
42897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.1ns 
42899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
45777      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
46763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
46771      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
46773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
46773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.8ns 
46774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
49705      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
50669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
50672      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.31ns 
50675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
50676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.5ns 
50677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
53558      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54512      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.81ns 
54516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.4ns 
54525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
57559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58606      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.9ms 
58619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 610.01ns 
58621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
61493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.96ms 
62465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.6ns 
62467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
65368      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66615      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 286.26ms 
66619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.9ns 
66620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
69562      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70496      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
70499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.11ns 
70501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
73394      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
74328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
74338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.2ns 
74340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
77213      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
78133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
78179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.21ms 
78182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
78182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.2ns 
78184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
81094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
82012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
82032      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.82ms 
82034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
82034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.23ns 
82035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
84929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85879      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.61ms 
85882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.2ns 
85888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
88785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
89720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
89722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
89722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns 
89724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
92605      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
93543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
93561      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.16ms 
93563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
93563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.9ns 
93564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
96455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
97375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
97407      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.65ms 
97409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
97410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.71ns 
97411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
100294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
101211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
101215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
101217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
101217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.21ns 
101219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
104065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
105035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
105084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.86ms 
105087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
105088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.61ns 
105089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
108063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
109102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
109195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.78ms 
109201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
109202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.21ns 
109204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
112066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
113023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
113078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.6ms 
113082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
113082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.9ns 
113083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
115966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
116919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
116928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
116931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
116932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.51ns 
116933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
119862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
120807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
120823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
120825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
120825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
120826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
123786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
124729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
124743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms 
124745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
124745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
124746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
127606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
128572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
128582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
128584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
128585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.9ns 
128586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
131415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
132367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
132377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
132380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
132380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.3ns 
132381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
135218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
136157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
136166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.88ms 
136168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
136168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.6ns 
136169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
139034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
139975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
139980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
139981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
139981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
139982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
142802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
143739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
143753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
143754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
143754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
143755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
146582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
147546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
147615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.89ms 
147618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
147618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.51ns 
147619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
150489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
151464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
151487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.62ms 
151489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
151489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.6ns 
151491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
154360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
155303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
155324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.08ms 
155326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
155326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139ns 
155327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
158145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
159084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
159106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.13ms 
159107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
159107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
159108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
161932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
162877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
162897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.61ms 
162900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
162900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.61ns 
162901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
165781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
166727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
166776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.58ms 
166777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
166777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns 
166778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
169674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
170628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
170634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
170638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
170639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 
170640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
173532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
174500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
174505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
174508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
174509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.81ns 
174510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
177369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
178320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
178330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
178331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
178332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
178332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
181182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
182123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
182133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
182135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
182135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
182136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
184972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
185934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
185970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.57ms 
185974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
185974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.41ns 
185976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
188817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
189756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
189766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
189767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
189767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
189768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
192606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
193621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
193629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
193633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
193634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.11ns 
193635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
196468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
197413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
197418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
197419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
197420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
197420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
200252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
201182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
201187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
201188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
201188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns 
201189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
204085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
204999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
205095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.85ms 
205098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
205098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.4ns 
205099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
207941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
208853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
208948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.41ms 
208950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
208950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188ns 
208951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
211819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
212730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
212734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
212736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
212736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
212737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
215599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
216514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
216555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.12ms 
216558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
216558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 498.51ns 
216559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
219399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
220310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
220343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.08ms 
220345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
220345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
220346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
223204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
224116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
224119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
224121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
224121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
224122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
226980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
227896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
228067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 159.98ms 
228070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
228070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.9ns 
228071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
230928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
231859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
231871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
231873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
231873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
231873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
234735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
235650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
235664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
235667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
235668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.1ns 
235669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
238593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
239502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
239522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.78ms 
239524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
239525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.1ns 
239526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
242366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
243284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
243304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
243309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
243309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.4ns 
243311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
246133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
247039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
247043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
247044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
247044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
247045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
249842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
250772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
250778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
250779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
250779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
250780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
253600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
254537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
254568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.8ms 
254570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
254570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
254571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
257398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
258345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
258368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 
258370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
258370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.6ns 
258371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
261201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
262140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
262157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
262160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
262160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.31ns 
262161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
264974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
265927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
265931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
265933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
265934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 
265935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
268757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
269731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
269739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
269742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
269742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.9ns 
269743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
272562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
273500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
273506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
273508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
273508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
273509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
276326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
277263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
277266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
277268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
277268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
277269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
280087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
281029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
281031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.21ns 
281033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
281033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
281033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
283905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
284863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
284867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
284869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
284869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
284870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
287695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
288637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
288640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
288641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
288641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
288642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
291478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
292414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
292483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.78ms 
292486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
292486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281ns 
292487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
295338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
296273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
296316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.84ms 
296317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
296317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
296318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
299141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
300080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
300113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.6ms 
300115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
300115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
300116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
302934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
303871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
303918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.36ms 
303920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
303920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
303921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
306784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
307729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
307763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.37ms 
307765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
307765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
307766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
310570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
311504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
311559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.88ms 
311560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
311560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
311561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
314368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
315315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
315346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.8ms 
315348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
315349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
315350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
318159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
319093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
319115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.56ms 
319116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
319116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
319117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
321928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
322869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
322897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.28ms 
322898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
322898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
322899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
325715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
326654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
326676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
326678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
326678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 
326679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
329493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
330430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
330460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.4ms 
330462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
330462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
330463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
333270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
334208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
334237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.32ms 
334238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
334238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
334239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
337060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
337998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
338027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.04ms 
338028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
338028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
338029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
340859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
341798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
341828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.25ms 
341830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
341830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
341831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
344638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
345574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
345599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.41ms 
345600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
345600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
345601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
348420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
349357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
349386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.21ms 
349388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
349388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
349389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
352233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
353193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
353226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.09ms 
353229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
353229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 
353230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
356053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
356992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
357002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
357004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
357004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
357005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
359899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
360881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
360902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.47ms 
360903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
360903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
360904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
363718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
364629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
364633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
364635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
364636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 
364637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
367477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
368387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
368389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.41ns 
368391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
368391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
368392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
371225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
372142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
372145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.11ns 
372146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
372146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
372147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
374994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
375903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
375912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
375919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
375920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262ns 
375921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
378754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
379659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
379666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
379668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
379668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
379669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
382496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
383412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
383427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
383428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
383428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
383429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
386268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
387182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
387186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
387187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
387188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
387188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
390027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
390938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
390941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.51ns 
390942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
390942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
390943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
393797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
394713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
394720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
394721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
394721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
394722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
397554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
398493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
398495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.11ns 
398497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
398497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
398497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
401338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
402283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
402290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.91ns 
402291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
402291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
402292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
405114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
406051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
406054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.11ns 
406055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
406055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
406056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
408889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
409828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
409833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
409834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
409834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
409835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
412656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
413599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
413609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.32ms 
413611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
413611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
413611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
416417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
417353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
417357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
417359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
417359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
417360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
420177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
421144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
421153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
421154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
421154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
421155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
423966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
424903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
424907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
424909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
424909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
424910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
427733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
428670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
428699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ms 
428702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
428702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 527.61ns 
428703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
431522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
432463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
432467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
432469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
432469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
432470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
435291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
436260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
436264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
436265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
436265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
436266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
439086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
440028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
440032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
440033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
440033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
440034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
442846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
443789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
443809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.92ms 
443811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
443811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
443812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
446667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
447611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
447617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.21ns 
447619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
447619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
447620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
450481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
451428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
451475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.32ms 
451477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
451477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
451478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
454331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
455282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
455286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
455288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
455288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
455288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
458167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
459111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
459137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.55ms 
459139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
459139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
459140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
462108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
463064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
463092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.95ms 
463095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
463095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
463096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
465971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
466927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
466966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.83ms 
466969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
466969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.8ns 
466970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
469984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
470943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
470946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.21ns 
470947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
470947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
470948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
473822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
474773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
474779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
474781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
474781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
474782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
477641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
478597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
478601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
478602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
478602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
478603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
481470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
482435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
482438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 965.81ns 
482439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
482439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
482440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
485342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
486300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
486303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
486307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
486307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.3ns 
486308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
489171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
490143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
490147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
490150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
490150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 
490151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
493028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
493957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
493960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
493962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
493962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
493963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
496837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
497764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
497777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
497779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
497779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
497779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
500664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
501599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
501614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
501615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
501615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
501616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
504499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
505424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
505437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ms 
505439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
505439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
505440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
508321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
509257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
509271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
509272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
509272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
509273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
512150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
513082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
513087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
513089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
513089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
513090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
515963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
516895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
516901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
516903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
516903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
516904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
519804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
520777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
520780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.41ns 
520781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
520781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
520782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
523663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
524596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
524600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
524601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
524601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
524602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
527472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
528403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
528411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
528413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
528414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.7ns 
528415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
531293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
532226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
532240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.99ms 
532242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
532242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
532242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
535125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
536060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
536065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
536066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
536066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
536067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
539008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
540018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
540026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
540027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
540027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
540028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
542876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
543832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
543835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.11ns 
543836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
543836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
543837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
546663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
547621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
547624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.51ns 
547625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
547625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
547626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
550447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
551407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
551412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
551413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
551413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
551414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
554239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
555206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
555209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
555211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
555211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
555211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
558171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
559206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
559210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
559212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
559212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
559212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
562036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
562996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
563000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
563001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
563001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
563002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
565840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
566798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
566805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
566806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
566806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
566807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
569674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
570610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
570613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
570615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
570615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
570616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
573479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
574410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
574424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
574426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
574427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
574428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
577271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
578195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
578235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.5ms 
578236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
578236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
578237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
581052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
582003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
582011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
582013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
582013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
582013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
584816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
585770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
585773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
585775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
585776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
585776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
588613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
589607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
589610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
589611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
589611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
589612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
592443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
593400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
593406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
593407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
593407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
593408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
596251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
597199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
597202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
597204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
597204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
597204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
600055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
601012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
601016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
601017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
601017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
601018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
603828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
604781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
604785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
604787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
604787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
604787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
607588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
608543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
608549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
608550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
608550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
608551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
611347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
612303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
612321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.51ms 
612322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
612322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
612323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
615161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
616087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
616105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.04ms 
616107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
616107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
616107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
618938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
619889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
619901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ms 
619902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
619902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
619903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
622708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
623658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
623671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.59ms 
623672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
623672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
623673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
626468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
627421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
627452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.09ms 
627454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
627454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
627455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
630280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
631204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
631234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.59ms 
631235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
631235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
631236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
634072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
635026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
635054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.88ms 
635056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
635056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
635057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
637861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
638815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
638832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
638833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
638833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
638834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
641660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
642619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
642655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.91ms 
642656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
642656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
642657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
645541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
646495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
646552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53ms 
646554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
646554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.6ns 
646555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
649411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
650368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
650413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.12ms 
650414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
650414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
650415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
653237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
654164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
654214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.61ms 
654215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
654215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
654216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
657066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
658023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
658075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.89ms 
658076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
658077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
658078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
660906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
661861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
662004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.84ms 
662006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
662006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
662007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
664875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
665801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
665813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
665815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
665815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
665816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
668639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
669592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
669601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
669603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
669603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.7ns 
669604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
672428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
673380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
673386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
673388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
673388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
673389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
676222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
677182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
677203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.08ms 
677204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
677204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
677205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
680008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
680960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
680973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
680974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
680974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
680975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
683790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
684712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
684716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
684718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
684718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
684718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
687529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
688483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
688503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ms 
688505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
688505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
688506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
691292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
692239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
692258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.44ms 
692260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
692260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
692261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
695068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
696035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
696058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.93ms 
696060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
696060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
696060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
698864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
699820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
699824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
699825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
699825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
699826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
702646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
703599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
703603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
703604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
703604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
703605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
706410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
707363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
707371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
707373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
707373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
707374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
710190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
711144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
711151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
711153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
711153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
711154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
713961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
714916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
714997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.47ms 
714999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
714999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
715000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
717841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
718798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
718832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.36ms 
718834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
718834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
718835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
721681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
722665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
722692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.87ms 
722693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
722693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
722694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
725605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
726561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
726563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 408.1ns 
726565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
726565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
726566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
729369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
730322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
730556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.22ms 
730558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
730558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 
730559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
733406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
734367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
734426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.46ms 
734428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
734428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.9ns 
734429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
737251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
738179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
738181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 378.3ns 
738183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
738183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
738183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
741017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
741969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
741971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 421.11ns 
741972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
741972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
741973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
744795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
745744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
745746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 442.11ns 
745747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
745747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
745748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
748541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
749491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
749494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.4ns 
749495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
749495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
749496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
752317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
753266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
753367     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
753383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.74ms 
753385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
753385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.2ns 
753386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
756219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
757147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
757208     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
757209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.08ms 
757211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
757211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
757213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
760107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
761083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
761084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
761115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
761167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
761195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
761203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
761213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
761216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
761218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
761220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
761223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
761225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
761227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
761228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
761445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
761447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
761448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
761450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
761451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
761643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
761644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
761645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
761647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
761648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
761649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
761808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
761810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
761812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
761813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
761814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
761815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
761939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
761941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
761942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
761943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
761944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
761945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
761952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
761953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
761954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
761956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
761957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
761958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
761965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
761966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
761967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
761969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
761969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
761970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
762116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
762117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
762119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
762248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
762249     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)'' 
762252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
762253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
762254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
762255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
762256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
762256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
762263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
762265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
762266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
762267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
762268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
762392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
762396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
762398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
762399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
762400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
762401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
762401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
762537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
762539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
762540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
762542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
762542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
762543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
762544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
762545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
762647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
762650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
762756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
762761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
762766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
762768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
762769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
762770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
762771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
762771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
762772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
762773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
762783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
762789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
762917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
762919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
762920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
762922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
762922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
762923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
762923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
762925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
762990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
762996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
763100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
763102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
763104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
763106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
763107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
763108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
763296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
763301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
763304     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)'' 
763306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
763308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
763310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
763311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
763312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
763321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
763332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
763334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
763335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
763445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
763447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
763448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
763448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
763450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
763451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
763571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
763573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
763574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
763576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
763577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
763577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
763578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
763581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
763681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
763683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
763774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
763775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
763776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
763781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
763785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
763790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
763939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
763941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
763942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
763943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
763957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
764073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
768541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
768542     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)'' 
768548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
768549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
768550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
768551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
768552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
768561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
768563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
768564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
768565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
768566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
768676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
768681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
768682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
768683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
768684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
768685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
768686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
768798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
768800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
768801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
768803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
768803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
768804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
768805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
768806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
768904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
768905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
769000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
769005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
769010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
769012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
769013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
769014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
769026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
769128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
769129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
769130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
769131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
769269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
769280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
769281     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)'' 
769283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
769284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
769285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
769286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
769286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
769299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
769301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
769302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
769303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
769304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
769407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
769409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
769410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
769411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
769412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
769519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
769525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
769527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
769527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
769528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
769529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
769530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
769644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
769646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
769647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
769648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
769649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
769649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
769649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
769651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
769652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
769652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
769654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
769654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
769655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
769655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
769656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
769758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
769759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
769766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
769857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
769950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
769951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
769952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
769953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
769954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
769954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
769955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
769955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
769956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
770056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
770063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
770167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
770168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
770169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
770170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
770171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
770171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
770171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
770172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
770178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
770179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
770272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
770278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
770284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
770400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
770401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
770402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
770403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
770403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
770404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
770404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
770405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
770468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
770469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
770470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
770471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
770472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
770478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
770484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
770622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
770726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
770727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
770728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
770729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
770924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
771028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
771029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
774708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
774715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
774716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
774717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
774718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
774856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
774858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
774860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
774861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
774862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
774987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
778508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
782277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
782283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
782284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
782285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
782286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
782418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
782420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
782421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
782423     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)' ...' 
782425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
783791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
783791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.9ns 
783792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
786637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
787621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
787622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
787623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
787643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
787663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
787666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
787668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
787669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
787674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
787676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
787679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
787682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
787683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
787694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
787696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
787696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
787753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
787754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
787755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
787756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
787756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
787826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
787827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
787828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
787829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
787830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
787834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
787834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
787835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
787836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
787837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
787837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
787925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
787926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
787927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
787928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
787929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
787929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
788076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
788076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
788077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
788077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
788078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
788079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
788079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
788079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
788080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
788081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
788081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
788081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
788082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
788082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
788083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
788083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
788084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
788085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
788085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
788088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
788126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
788128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
788186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
788187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
788189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
788190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
788191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
788191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
788244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
788247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
788248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
788249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
788251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
788251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
788252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
788302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
788305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
788308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
788367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
788427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
788427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
788428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
791264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
792226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
792263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.79ms