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

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

tests
0

failures
0

ignored
11m41.23s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.299s passed
powPositiveConcrete data()[101] 3.433s passed
powGeq1Concrete data()[102] 3.671s passed
pow2InIntLower data()[103] 3.414s passed
pow2InIntUpper data()[104] 3.586s passed
logSelfConcrete data()[105] 3.522s passed
log1Concrete data()[106] 3.371s passed
logProduct data()[107] 3.360s passed
logTimesBaseConcrete data()[108] 3.484s passed
logProdIdentity data()[109] 3.599s passed
moduloByteIsInByte data()[10] 3.742s passed
logProdIdentityConcrete data()[110] 3.500s passed
logPowIdentity data()[111] 3.310s passed
logPowIdentityConcrete data()[112] 3.303s passed
logPositive data()[113] 3.167s passed
logPositiveConcrete data()[114] 3.346s passed
logMono data()[115] 3.239s passed
logMonoConcrete data()[116] 3.291s passed
powLogLess data()[117] 3.320s passed
powLogMore2 data()[118] 3.206s passed
logLessThanPow data()[119] 3.335s passed
moduloCharIsInChar data()[11] 3.624s passed
logLessThanPowConcrete data()[120] 3.417s passed
logSqueeze data()[121] 3.144s passed
ifthenelse_equals data()[122] 3.257s passed
ifthenelse_equals_1 data()[123] 3.324s passed
ifthenelse_equals_2 data()[124] 3.426s passed
disjointWithSingleton1 data()[125] 3.229s passed
disjointWithSingleton2 data()[126] 3.294s passed
disjointArrayRanges data()[127] 3.371s passed
disjointArrayRangeAllFields1 data()[128] 3.313s passed
disjointArrayRangeAllFields2 data()[129] 3.414s passed
div_unique1 data()[12] 3.639s passed
seqSelfDefinition data()[130] 3.433s passed
seqOutsideValue data()[131] 3.382s passed
castedGetAny data()[132] 3.324s passed
seqGetAlphaCast data()[133] 3.337s passed
getOfSeqSingleton data()[134] 3.448s passed
getOfSeqSingletonConcrete data()[135] 3.233s passed
getOfSeqConcat data()[136] 3.259s passed
getOfSeqSub data()[137] 3.501s passed
getOfSeqReverse data()[138] 3.541s passed
lenOfSeqEmpty data()[139] 3.280s passed
div_unique2 data()[13] 3.537s passed
lenOfSeqSingleton data()[140] 3.257s passed
lenOfSeqConcat data()[141] 3.267s passed
lenOfSeqSub data()[142] 3.294s passed
lenOfSeqReverse data()[143] 3.377s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.325s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.372s passed
getOfSeqSingletonEQ data()[146] 3.329s passed
getOfSeqConcatEQ data()[147] 3.370s passed
getOfSeqSubEQ data()[148] 3.346s passed
getOfSeqReverseEQ data()[149] 3.356s passed
div_exists data()[14] 3.740s passed
lenOfSeqEmptyEQ data()[150] 3.330s passed
lenOfSeqSingletonEQ data()[151] 3.434s passed
lenOfSeqConcatEQ data()[152] 3.338s passed
lenOfSeqSubEQ data()[153] 3.312s passed
lenOfSeqReverseEQ data()[154] 3.340s passed
getOfSeqDefEQ data()[155] 3.391s passed
lenOfSeqDefEQ data()[156] 3.555s passed
seqConcatWithSeqEmpty1 data()[157] 3.578s passed
seqConcatWithSeqEmpty2 data()[158] 3.417s passed
seqReverseOfSeqEmpty data()[159] 3.395s passed
div_one data()[15] 3.650s passed
subSeqComplete data()[160] 3.365s passed
subSeqTailR data()[161] 3.514s passed
subSeqTailL data()[162] 3.460s passed
subSeqTailEQR data()[163] 3.623s passed
subSeqTailEQL data()[164] 3.506s passed
seqDef_split data()[165] 3.502s passed
seqDef_induction_upper data()[166] 3.368s passed
seqDef_induction_upper_concrete data()[167] 3.335s passed
seqDef_induction_lower data()[168] 3.311s passed
seqDef_induction_lower_concrete data()[169] 3.251s passed
jdiv_one data()[16] 3.476s passed
seqDef_split_in_three data()[170] 3.399s passed
seqDef_empty data()[171] 3.336s passed
seqDef_one_summand data()[172] 3.346s passed
seqDef_lower_equals_upper data()[173] 3.422s passed
seqDefOfSeq data()[174] 3.389s passed
seqSelfDefinitionEQ2 data()[175] 3.262s passed
indexOfSeqSingleton data()[176] 3.177s passed
indexOfSeqConcatFirst data()[177] 3.200s passed
indexOfSeqConcatSecond data()[178] 3.404s passed
indexOfSeqSub data()[179] 3.317s passed
div_zero data()[17] 3.529s passed
lenOfArray2seq data()[180] 3.439s passed
getAnyOfArray2seq data()[181] 3.383s passed
getOfArray2seq data()[182] 3.293s passed
getAnyOfNPermInv data()[183] 3.311s passed
seqNPermRange data()[184] 3.510s passed
seqPermTrans data()[185] 3.345s passed
seqPermRefl data()[186] 3.267s passed
seqPermSplit data()[187] 3.422s passed
seqNPermRight data()[188] 3.678s passed
seqPermFromSwap data()[189] 3.389s passed
divResZero1 data()[18] 3.554s passed
seqPermTransAlt0 data()[190] 3.328s passed
seqPermTransAlt1 data()[191] 3.482s passed
seqPermTransAlt2 data()[192] 3.526s passed
seqPermTransAlt3 data()[193] 3.600s passed
seqPermForall data()[194] 3.396s passed
seqPermExists data()[195] 3.467s passed
schiffl_lemma_2 data()[196] 24.335s passed
schiffl_thm_1 data()[197] 4.295s passed
eqSameSeq data()[198] 3.465s passed
divResZero2 data()[19] 3.586s passed
eqTermCut data()[1] 4.359s passed
divResOne1 data()[20] 3.644s passed
divResOne2 data()[21] 3.475s passed
div_cancel1 data()[22] 3.421s passed
div_cancel2 data()[23] 3.465s passed
divAddMultDenom data()[24] 3.424s passed
divMinus data()[25] 3.472s passed
divMinusDenom data()[26] 3.536s passed
divLeastDPos data()[27] 3.409s passed
divLeastDNeg data()[28] 3.369s passed
divGreatestDPos data()[29] 3.508s passed
equivAllRight data()[2] 3.789s passed
divGreatestDNeg data()[30] 3.430s passed
divIncreasingPos data()[31] 3.387s passed
divIncreasingNeg data()[32] 3.558s passed
jdiv_zero data()[33] 3.498s passed
jdivPulloutMinusNum data()[34] 3.525s passed
jdivPulloutMinusDenom data()[35] 3.519s passed
jdiv_uniquePosPos data()[36] 3.417s passed
jdiv_uniquePosNeg data()[37] 3.556s passed
jdiv_uniqueNegPos data()[38] 3.479s passed
jdiv_uniqueNegNeg data()[39] 3.358s passed
irrflConcrete1 data()[3] 3.891s passed
jdivMultDenom1 data()[40] 3.598s passed
jdivMultDenom2 data()[41] 3.399s passed
mod_geZero data()[42] 3.420s passed
mod_lessDenom data()[43] 3.442s passed
jmod_NumPos data()[44] 3.431s passed
jmod_NumNeg data()[45] 3.529s passed
jmod_geZero data()[46] 3.687s passed
jmodNumZero data()[47] 3.651s passed
jmod_pulloutminusNum data()[48] 3.661s passed
jmod_pulloutminusDenom data()[49] 3.601s passed
irrflConcrete2 data()[4] 3.774s passed
jmodUnique1 data()[50] 3.731s passed
jmodUnique2 data()[51] 3.755s passed
intDivRem data()[52] 3.506s passed
jmodjmod data()[53] 3.439s passed
jmodDivisible data()[54] 3.512s passed
jmodDivisibleRep data()[55] 3.487s passed
jdivAddMultDenom data()[56] 3.610s passed
jmodAltZero data()[57] 3.387s passed
jmodAddMultDenomZero data()[58] 3.377s passed
polyDiv_zero data()[59] 3.404s passed
cancel_gtPos data()[5] 3.688s passed
polyMod_ltdivDenom data()[60] 3.341s passed
bsum_empty data()[61] 3.214s passed
bsum_induction_upper data()[62] 3.222s passed
bsum_induction_lower data()[63] 3.290s passed
bsum_num_of_bounds data()[64] 3.396s passed
bsum_num_of_bounds2 data()[65] 3.462s passed
bsum_induction_upper2 data()[66] 3.335s passed
bsum_induction_upper_concrete data()[67] 3.442s passed
bsum_induction_upper_concrete_2 data()[68] 3.296s passed
bsum_induction_upper2_concrete data()[69] 3.430s passed
cancel_gtNeg data()[6] 3.656s passed
bsum_induction_lower_concrete data()[70] 3.475s passed
bsum_induction_lower2 data()[71] 3.498s passed
bsum_induction_lower2_concrete data()[72] 3.369s passed
bsum_positive data()[73] 3.341s passed
bsum_upper_bound data()[74] 3.456s passed
bsum_lower_bound data()[75] 3.459s passed
bsum_positive_lower_bound_element data()[76] 3.435s passed
bsum_sub_same_index data()[77] 3.344s passed
bsum_less_same_index data()[78] 3.388s passed
bsum_equal_except_one_index data()[79] 3.310s passed
moduloIntIsInInt data()[7] 3.665s passed
bsum_num_of_is_max data()[80] 3.352s passed
bsum_num_of_is_max2 data()[81] 3.419s passed
bsum_num_of_is_max3 data()[82] 3.545s passed
bsum_num_of_is_max4 data()[83] 3.469s passed
bsum_num_of_lt_max data()[84] 3.456s passed
bsum_num_of_lt_max2 data()[85] 3.344s passed
bsum_num_of_lt_max3 data()[86] 3.355s passed
bsum_num_of_lt_max4 data()[87] 3.394s passed
bsum_num_of_gt0 data()[88] 3.331s passed
bsum_num_of_gt0_alt data()[89] 3.288s passed
moduloLongIsInLong data()[8] 3.522s passed
bsum_add_concrete data()[90] 3.386s passed
bprod_all_positive data()[91] 3.346s passed
bprod_split data()[92] 3.347s passed
powConcrete0 data()[93] 3.196s passed
powConcrete1 data()[94] 3.311s passed
powSplitFactor data()[95] 3.319s passed
powAdd data()[96] 3.440s passed
powMono data()[97] 3.260s passed
powMonoConcrete data()[98] 3.354s passed
powMonoConcreteRight data()[99] 3.269s passed
moduloShortIsInShort data()[9] 3.566s passed

Standard output

404        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
426        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.13ms 
651        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665        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)

1634       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1636       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1643       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1652       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3098       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8711       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.06s 
8771       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8808       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ns 
8820       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8820       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.61ns 
8824       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
12088      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13170      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.11ms 
13186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.31ns 
13188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16019      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
16019      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16972      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
16974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.61ns 
16976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19913      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
19914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
20865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20866      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.54ns 
20867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
23678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
24622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
24639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.51ns 
24641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
27393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28324      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.12ms 
28330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 568.05ns 
28333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
31001      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.11ms 
31986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.51ns 
31987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34747      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
34747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
35645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
35649      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 857.17ns 
35650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
35651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.31ns 
35652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
38296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
39168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
39171      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.66ns 
39174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
39174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.43ns 
39175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
41859      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
42734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
42737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 586.25ns 
42740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
42740      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.23ns 
42742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
45580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
46476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
46479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.25ns 
46481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
46481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.11ns 
46483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49191      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
49191      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
50097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
50102      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 788.87ns 
50106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
50106      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.14ns 
50108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
52813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
53687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
53743      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.81ms 
53749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
53749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.71ns 
53750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56356      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
56357      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
57244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
57283      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.55ms 
57286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
57287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.84ns 
57288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
59937      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
60821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
61023      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.43ms 
61026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
61026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.91ns 
61027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
63774      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
64668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
64674      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
64676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
64676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.61ns 
64677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
67270      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
68144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
68150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
68154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
68155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 597.35ns 
68158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
70813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
71639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
71681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.71ms 
71683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
71684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.83ns 
71685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
74335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
75218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
75235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
75238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
75238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.13ns 
75239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
77894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
78805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
78821      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
78823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
78824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.93ns 
78825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
81594      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
82447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
82465      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms 
82468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
82468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.52ns 
82469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85102      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
85102      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
85924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
85939      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
85942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
85942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.53ns 
85944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
88517      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
89332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
89360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.16ms 
89363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
89363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.23ns 
89365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
91924      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
92823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
92826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
92829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
92829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.83ns 
92830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
95368      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
96206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
96250      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.04ms 
96253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
96253      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.13ns 
96254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98791      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
98792      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
99645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
99719      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.28ms 
99724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
99724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.51ns 
99725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
102335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
103215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
103258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.21ms 
103259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
103259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.81ns 
103260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
105804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
106659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
106667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
106670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
106670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.33ns 
106671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
109167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
110015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
110036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
110038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
110039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.43ns 
110040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
112691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
113531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
113544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
113546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
113546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.51ns 
113576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
116142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
116963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
116974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.61ms 
116978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
116978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.83ns 
116979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
119530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
120356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
120363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
120365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
120365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.53ns 
120366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
122940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
123915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
123921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
123923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
123923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.41ns 
123924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
126534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
127415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
127419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
127420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
127420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.91ns 
127421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
130047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
130919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
130936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.55ms 
130947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
130947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.53ns 
130951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
133586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
134410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
134462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.32ms 
134465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
134465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.63ns 
134466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
137007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
137863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
137880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
137882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
137882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.52ns 
137883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
140557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
141418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
141436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.73ms 
141439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
141439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.63ns 
141440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
144046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
144889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
144916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.19ms 
144917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
144917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.41ns 
144918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
147460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
148255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
148273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
148275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
148275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.31ns 
148276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
150963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
151827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
151871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.72ms 
151872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
151872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.71ns 
151873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
154460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
155267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
155270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
155272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
155272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.51ns 
155272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
157847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
158686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
158690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
158692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
158692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.01ns 
158693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
161269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
162123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
162132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
162133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
162133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.21ns 
162134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
164699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
165555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
165563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
165565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
165565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.41ns 
165566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
168175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
169072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
169092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
169094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
169094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.41ns 
169095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
171878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
172770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
172780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
172781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
172781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.11ns 
172782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
175446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
176426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
176430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
176434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
176434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.82ns 
176435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
179172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
180087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
180092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
180093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
180093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.71ns 
180094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
182815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
183687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
183692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
183693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
183694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.11ns 
183695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
186419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
187293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
187423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 121.32ms 
187430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
187430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
187431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
190240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
191093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
191182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.75ms 
191185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
191186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.03ns 
191187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
193835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
194686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
194690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
194691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
194691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.71ns 
194692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
197235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
198090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
198128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.98ms 
198130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
198130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.92ns 
198131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
200734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
201606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
201640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.34ms 
201641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
201641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.01ns 
201642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
204201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
205123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
205127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
205133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
205134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.32ns 
205135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
207777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
208587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
208740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 142.34ms 
208742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
208742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.81ns 
208743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
211289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
212115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
212127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
212129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
212129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.21ns 
212129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
214660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
215496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
215505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
215506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
215506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.21ns 
215507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
218038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
218890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
218908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
218909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
218910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.91ns 
218910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
221425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
222235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
222249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.59ms 
222251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
222251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.41ns 
222252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
224677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
225460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
225463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
225465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
225465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.91ns 
225466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
227898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
228680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
228686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
228687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
228687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.61ns 
228688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
231108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
231937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
231974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.68ms 
231977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
231977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.21ns 
231978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
234483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
235351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
235371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.04ms 
235374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
235374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.62ns 
235375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
237987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
238817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
238834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
238836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
238836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.92ns 
238837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
241314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
242165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
242169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
242171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
242171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.01ns 
242172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
244734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
245607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
245611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
245613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
245613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
245613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
248093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
248900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
248907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
248908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
248909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.81ns 
248909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
251528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
252334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
252337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
252338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
252339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
252339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
254969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
255810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
255812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.96ns 
255814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
255814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
255815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
258460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
259305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
259310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
259311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
259311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
259312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
261823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
262677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
262680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
262681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
262681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
262682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
265148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
265968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
266020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.2ms 
266022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
266022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.81ns 
266023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
268571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
269431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
269477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.74ms 
269478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
269478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.61ns 
269479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
272047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
272892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
272935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.29ms 
272938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
272938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.91ns 
272939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
275506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
276322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
276371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.47ms 
276372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
276372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.71ns 
276373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
278853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
279677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
279714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.82ms 
279715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
279716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
279716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
282186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
283035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
283102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.79ms 
283104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
283104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.41ns 
283105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
285607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
286377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
286412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.87ms 
286414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
286414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
286415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
288942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
289739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
289765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.28ms 
289769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
289770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.62ns 
289770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
292294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
293153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
293186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.02ms 
293187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
293187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
293188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
295892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
296710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
296732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.01ms 
296733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
296733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.81ns 
296734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
299293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
300166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
300200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.42ms 
300202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
300203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.32ns 
300204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
302753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
303626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
303656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.34ms 
303658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
303658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.01ns 
303659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
306129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
306970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
307001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.2ms 
307002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
307002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
307003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
309500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
310330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
310355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.35ms 
310356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
310356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
310357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
312870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
313725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
313749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
313751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
313751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
313752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
316244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
317054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
317080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
317082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
317082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.02ns 
317083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
319509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
320338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
320368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.67ms 
320370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
320371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.72ns 
320372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
322928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
323746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
323755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
323756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
323756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
323757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
326295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
327081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
327101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.63ms 
327102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
327102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
327103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
329619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
330443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
330448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
330449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
330449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.91ns 
330450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
332832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
333640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
333643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.85ns 
333644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
333645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
333645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
336110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
336952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
336955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 861.56ns 
336956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
336956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
336957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
339425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
340259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
340272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
340276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
340276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns 
340277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
342824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
343707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
343714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
343716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
343716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
343716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
346158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
346962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
346975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
346976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
346976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
346977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
349491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
350324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
350328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
350329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
350329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
350330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
352820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
353595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
353597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.85ns 
353598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
353598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
353599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
356065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
356890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
356896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
356897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
356898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
356898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
359499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
360327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
360329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.95ns 
360331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
360331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
360331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
363067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
363998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
364000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.33ns 
364002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
364002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
364002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
366532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
367412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
367414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.54ns 
367416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
367416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
367417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
370083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
370995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
370999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
371002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
371002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.41ns 
371003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
373626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
374512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
374522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
374524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
374525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.22ns 
374526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
377016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
377889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
377894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
377895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
377895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
377896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
380409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
381245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
381253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
381255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
381255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.22ns 
381256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
383872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
384733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
384737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
384739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
384739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
384740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
387480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
388313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
388336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.25ms 
388339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
388339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.21ns 
388340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
391008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
391833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
391837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
391838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
391838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
391839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
394381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
395144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
395147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
395148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
395148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
395149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
397620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
398445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
398449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
398451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
398451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
398451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
400808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
401598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
401616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
401617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
401617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
401618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
404137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
404957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
404962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.02ns 
404964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
404964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
404965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
407337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
408151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
408201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.37ms 
408203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
408203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
408204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
410665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
411488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
411492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
411493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
411493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
411494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
413990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
414791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
414812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.92ms 
414814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
414814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
414815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
417191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
417994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
418018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.39ms 
418021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
418021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.12ns 
418022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
420476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
421326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
421354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.23ms 
421356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
421356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
421357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
423972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
424769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
424772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.04ns 
424773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
424773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
424774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
427148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
427909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
427915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
427916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
427917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
427917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
430376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
431169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
431172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
431173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
431173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
431174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
433612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
434493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
434496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.65ns 
434499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
434499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 756.14ns 
434500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
437086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
437919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
437922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 903.95ns 
437923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
437923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
437924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
440322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
441147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
441151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
441152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
441152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
441153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
443641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
444441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
444445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
444447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
444447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.21ns 
444448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
446953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
447803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
447815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
447818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
447818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
447819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
450288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
451110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
451129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
451131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
451132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.12ns 
451133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
453713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
454528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
454544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ms 
454545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
454545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
454546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
457118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
457956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
457977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 
457978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
457978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
457979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
460507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
461354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
461359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
461360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
461360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
461361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
463823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
464677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
464682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
464684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
464684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
464684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
467182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
468017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
468020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 989.86ns 
468021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
468021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
468022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
470617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
471464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
471467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
471469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
471469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
471469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
473897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
474698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
474701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.35ns 
474702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
474702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
474703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
477135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
477947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
477959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.15ms 
477961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
477961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
477961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
480526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
481455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
481460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
481461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
481462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
481463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
484150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
484994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
485001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.89ms 
485003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
485003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
485003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
487457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
488279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
488282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.05ns 
488283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
488283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
488284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
490725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
491536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
491538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.04ns 
491540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
491540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
491540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
493961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
494802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
494805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
494806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
494807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.21ns 
494807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
497231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
498096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
498100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
498101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
498101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
498102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
500643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
501471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
501476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
501478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
501478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.41ns 
501479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
503962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
504798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
504801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
504802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
504802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
504803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
507292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
508167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
508173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
508174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
508174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
508175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
510676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
511499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
511502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
511503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
511503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
511504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
514034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
514859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
514872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
514874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
514874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.91ns 
514875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
517343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
518216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
518218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.14ns 
518220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
518220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
518221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
520714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
521567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
521574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
521576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
521576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
521576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
524079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
524902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
524904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
524905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
524905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
524906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
527441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
528333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
528337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
528340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
528340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.51ns 
528341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
530825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
531671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
531676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
531677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
531677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
531678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
534100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
534984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
534988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
534990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
534990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.11ns 
534991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
537477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
538325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
538329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
538330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
538330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
538330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
540837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
541715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
541719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
541721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
541721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
541721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
544401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
545269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
545275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
545276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
545276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
545277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
547910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
548836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
548852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
548853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
548853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
548854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
551440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
552252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
552269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.38ms 
552270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
552270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
552271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
554807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
555653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
555665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
555666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
555666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
555667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
558150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
559018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
559029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
559031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
559031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
559031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
561612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
562515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
562543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.84ms 
562545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
562545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
562546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
565083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
565975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
566003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.11ms 
566004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
566005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
566005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
568694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
569599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
569626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.74ms 
569628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
569628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
569628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
572260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
573116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
573132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
573133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
573133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
573134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
575768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
576602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
576634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.7ms 
576636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
576636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.11ns 
576637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
579119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
579951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
580002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.13ms 
580004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
580004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
580005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
582439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
583289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
583337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.38ms 
583339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
583339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.41ns 
583341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
585775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
586602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
586648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.01ms 
586649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
586649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
586650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
589038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
589855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
589899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.02ms 
589900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
589900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
589901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
592340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
593117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
593298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 169.2ms 
593300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
593300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.91ns 
593301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
595774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
596626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
596634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
596635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
596636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
596636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
599136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
599969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
599981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
599982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
599982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
599982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
602491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
603396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
603402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
603403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
603403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
603404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
605954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
606775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
606792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
606793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
606793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
606794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
609227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
610042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
610054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
610055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
610055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
610055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
612416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
613227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
613230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
613232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
613232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
613232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
615618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
616411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
616430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.03ms 
616432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
616432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
616433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
618986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
619815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
619834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.09ms 
619835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
619835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
619836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
622286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
623130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
623151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.08ms 
623153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
623153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
623153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
625701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
626587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
626591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
626592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
626592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
626593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
629087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
629968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
629974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
629975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
629975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
629976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
632412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
633259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
633267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
633268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
633268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
633269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
635745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
636571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
636577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
636578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
636578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
636579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
639149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
640008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
640087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.67ms 
640089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
640089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
640089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
642591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
643405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
643433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.47ms 
643434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
643434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
643435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
645872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
646676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
646700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.59ms 
646701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
646701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
646702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
649206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
650119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
650121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 373.92ns 
650122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
650123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
650124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
652761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
653590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
653799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.32ms 
653801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
653801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
653802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
656290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
657133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
657188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.94ms 
657191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
657191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
657191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
659620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
660515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
660517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 368.32ns 
660521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
660521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.92ns 
660522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
663127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
663998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
664000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.62ns 
664001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
664001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
664002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
666618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
667524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
667526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 409.92ns 
667528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
667529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
667529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
670243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
671125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
671127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.92ns 
671128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
671128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
671129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
673587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
674406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
674501     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
674523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.22ms 
674525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
674525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.91ns 
674527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
677083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
677935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
677989     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
677990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.42ms 
677992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
677992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
677993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
680578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
681439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
681441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
681472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
681508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
681526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
681531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
681537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
681540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
681541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
681543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
681551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
681554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
681556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
681557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
681786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
681788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
681789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
681791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
681792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
681944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
681945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
681949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
681951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
681952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
681953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
682151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
682153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
682155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
682156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
682158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
682160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
682312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
682314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
682316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
682317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
682318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
682320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
682333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
682334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
682335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
682337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
682339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
682340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
682350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
682351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
682352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
682353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
682354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
682355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
682504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
682505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
682507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
682645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
682647     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)'' 
682650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
682651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
682652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
682654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
682655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
682658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
682662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
682664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
682666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
682667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
682667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
682787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
682791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
682793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
682794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
682796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
682797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
682799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
682939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
682941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
682942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
682944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
682945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
682946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
682948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
682950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
683056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
683058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
683171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
683175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
683181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
683182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
683185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
683186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
683187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
683187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
683188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
683190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
683201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
683206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
683328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
683330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
683332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
683334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
683334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
683335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
683336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
683337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
683398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
683406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
683517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
683519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
683522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
683523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
683524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
683525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
683685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
683690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
683693     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)'' 
683696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
683698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
683699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
683699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
683700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
683711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
683717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
683719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
683719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
683859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
683861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
683862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
683864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
683864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
683866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
684035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
684037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
684039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
684041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
684042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
684043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
684044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
684046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
684139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
684140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
684225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
684226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
684227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
684231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
684241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
684247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
684414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
684416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
684417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
684419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
684432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
684531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
688306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
688307     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)'' 
688312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
688313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
688314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
688315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
688317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
688326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
688327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
688328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
688329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
688329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
688434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
688438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
688440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
688440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
688441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
688442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
688442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
688547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
688549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
688550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
688553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
688554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
688554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
688555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
688556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
688637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
688638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
688719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
688723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
688728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
688729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
688729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
688730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
688741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
688828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
688829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
688830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
688831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
688909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
688920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
688920     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)'' 
688922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
688923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
688924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
688925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
688926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
688937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
688939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
688940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
688941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
688941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
689036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
689038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
689040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
689040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
689041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
689143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
689148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
689149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
689150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
689151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
689151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
689152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
689256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
689257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
689258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
689259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
689260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
689261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
689261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
689262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
689263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
689264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
689265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
689265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
689266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
689266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
689267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
689366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
689367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
689377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
689465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
689551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
689552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
689553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
689554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
689555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
689555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
689556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
689556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
689557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
689648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
689654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
689802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
689805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
689806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
689807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
689808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
689808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
689809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
689810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
689816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
689817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
689900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
689907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
689912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
690018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
690019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
690020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
690021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
690022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
690023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
690023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
690024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
690081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
690081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
690082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
690083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
690084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
690090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
690095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
690221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
690319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
690320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
690320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
690321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
690511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
690613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
690614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
693849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
693855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
693856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
693857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
693857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
693988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
693990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
693991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
693992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
693993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
694128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
697587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
700966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
700971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
700972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
700973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
700974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
701096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
701098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
701099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
701100     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)' ...' 
701102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
702327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
702327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
702328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
704960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
705860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
705861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
705862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
705868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
705881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
705884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
705886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
705886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
705890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
705892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
705895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
705897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
705898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
705906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
705908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
705908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
705955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
705956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
705956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
705957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
705957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
706023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
706024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
706025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
706026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
706026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
706030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
706031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
706031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
706032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
706033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
706034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
706120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
706121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
706122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
706123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
706124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
706125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
706222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
706223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
706224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
706225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
706225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
706226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
706227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
706227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
706229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
706229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
706230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
706230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
706231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
706231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
706232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
706233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
706233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
706235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
706236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
706238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
706281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
706283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
706352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
706353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
706355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
706357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
706358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
706358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
706414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
706417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
706418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
706420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
706421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
706422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
706422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
706480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
706483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
706486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
706553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
706622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
706622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.91ns 
706623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
709183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
710051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
710085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.12ms