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

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

tests
0

failures
0

ignored
10m6.57s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 2.918s passed
powPositiveConcrete data()[101] 2.921s passed
powGeq1Concrete data()[102] 2.938s passed
pow2InIntLower data()[103] 2.924s passed
pow2InIntUpper data()[104] 2.926s passed
logSelfConcrete data()[105] 2.916s passed
log1Concrete data()[106] 2.918s passed
logProduct data()[107] 2.937s passed
logTimesBaseConcrete data()[108] 2.928s passed
logProdIdentity data()[109] 2.937s passed
moduloByteIsInByte data()[10] 2.998s passed
logProdIdentityConcrete data()[110] 2.935s passed
logPowIdentity data()[111] 2.923s passed
logPowIdentityConcrete data()[112] 2.929s passed
logPositive data()[113] 2.932s passed
logPositiveConcrete data()[114] 2.928s passed
logMono data()[115] 2.945s passed
logMonoConcrete data()[116] 2.913s passed
powLogLess data()[117] 2.940s passed
powLogMore2 data()[118] 2.969s passed
logLessThanPow data()[119] 2.938s passed
moduloCharIsInChar data()[11] 2.980s passed
logLessThanPowConcrete data()[120] 2.937s passed
logSqueeze data()[121] 2.959s passed
ifthenelse_equals data()[122] 2.923s passed
ifthenelse_equals_1 data()[123] 2.927s passed
ifthenelse_equals_2 data()[124] 2.926s passed
disjointWithSingleton1 data()[125] 2.946s passed
disjointWithSingleton2 data()[126] 2.932s passed
disjointArrayRanges data()[127] 2.934s passed
disjointArrayRangeAllFields1 data()[128] 2.937s passed
disjointArrayRangeAllFields2 data()[129] 2.925s passed
div_unique1 data()[12] 3.025s passed
seqSelfDefinition data()[130] 2.966s passed
seqOutsideValue data()[131] 2.940s passed
castedGetAny data()[132] 2.931s passed
seqGetAlphaCast data()[133] 2.923s passed
getOfSeqSingleton data()[134] 2.949s passed
getOfSeqSingletonConcrete data()[135] 2.931s passed
getOfSeqConcat data()[136] 2.934s passed
getOfSeqSub data()[137] 2.969s passed
getOfSeqReverse data()[138] 2.937s passed
lenOfSeqEmpty data()[139] 2.928s passed
div_unique2 data()[13] 3.010s passed
lenOfSeqSingleton data()[140] 2.955s passed
lenOfSeqConcat data()[141] 2.937s passed
lenOfSeqSub data()[142] 2.933s passed
lenOfSeqReverse data()[143] 2.945s passed
equalityToSeqGetAndSeqLenLeft data()[144] 2.935s passed
equalityToSeqGetAndSeqLenRight data()[145] 2.931s passed
getOfSeqSingletonEQ data()[146] 2.947s passed
getOfSeqConcatEQ data()[147] 2.939s passed
getOfSeqSubEQ data()[148] 2.932s passed
getOfSeqReverseEQ data()[149] 2.951s passed
div_exists data()[14] 3.203s passed
lenOfSeqEmptyEQ data()[150] 2.927s passed
lenOfSeqSingletonEQ data()[151] 2.945s passed
lenOfSeqConcatEQ data()[152] 2.931s passed
lenOfSeqSubEQ data()[153] 2.964s passed
lenOfSeqReverseEQ data()[154] 3.027s passed
getOfSeqDefEQ data()[155] 2.984s passed
lenOfSeqDefEQ data()[156] 2.937s passed
seqConcatWithSeqEmpty1 data()[157] 2.950s passed
seqConcatWithSeqEmpty2 data()[158] 2.941s passed
seqReverseOfSeqEmpty data()[159] 2.947s passed
div_one data()[15] 3.017s passed
subSeqComplete data()[160] 2.952s passed
subSeqTailR data()[161] 2.972s passed
subSeqTailL data()[162] 2.953s passed
subSeqTailEQR data()[163] 2.972s passed
subSeqTailEQL data()[164] 2.942s passed
seqDef_split data()[165] 2.963s passed
seqDef_induction_upper data()[166] 2.990s passed
seqDef_induction_upper_concrete data()[167] 2.958s passed
seqDef_induction_lower data()[168] 2.991s passed
seqDef_induction_lower_concrete data()[169] 2.988s passed
jdiv_one data()[16] 2.986s passed
seqDef_split_in_three data()[170] 3.036s passed
seqDef_empty data()[171] 2.948s passed
seqDef_one_summand data()[172] 2.947s passed
seqDef_lower_equals_upper data()[173] 2.935s passed
seqDefOfSeq data()[174] 2.960s passed
seqSelfDefinitionEQ2 data()[175] 2.951s passed
indexOfSeqSingleton data()[176] 2.933s passed
indexOfSeqConcatFirst data()[177] 2.977s passed
indexOfSeqConcatSecond data()[178] 3.059s passed
indexOfSeqSub data()[179] 3.061s passed
div_zero data()[17] 3.042s passed
lenOfArray2seq data()[180] 3.022s passed
getAnyOfArray2seq data()[181] 3.004s passed
getOfArray2seq data()[182] 2.946s passed
getAnyOfNPermInv data()[183] 2.961s passed
seqNPermRange data()[184] 3.013s passed
seqPermTrans data()[185] 2.981s passed
seqPermRefl data()[186] 2.938s passed
seqPermSplit data()[187] 2.943s passed
seqNPermRight data()[188] 3.151s passed
seqPermFromSwap data()[189] 3.058s passed
divResZero1 data()[18] 2.979s passed
seqPermTransAlt0 data()[190] 2.950s passed
seqPermTransAlt1 data()[191] 2.942s passed
seqPermTransAlt2 data()[192] 2.940s passed
seqPermTransAlt3 data()[193] 2.942s passed
seqPermForall data()[194] 3.038s passed
seqPermExists data()[195] 3.010s passed
schiffl_lemma_2 data()[196] 20.539s passed
schiffl_thm_1 data()[197] 3.806s passed
eqSameSeq data()[198] 3.086s passed
divResZero2 data()[19] 2.973s passed
eqTermCut data()[1] 3.609s passed
divResOne1 data()[20] 2.981s passed
divResOne2 data()[21] 2.979s passed
div_cancel1 data()[22] 2.962s passed
div_cancel2 data()[23] 2.986s passed
divAddMultDenom data()[24] 2.996s passed
divMinus data()[25] 3.013s passed
divMinusDenom data()[26] 2.999s passed
divLeastDPos data()[27] 2.951s passed
divLeastDNeg data()[28] 2.955s passed
divGreatestDPos data()[29] 2.981s passed
equivAllRight data()[2] 3.271s passed
divGreatestDNeg data()[30] 2.958s passed
divIncreasingPos data()[31] 2.966s passed
divIncreasingNeg data()[32] 2.952s passed
jdiv_zero data()[33] 2.964s passed
jdivPulloutMinusNum data()[34] 2.962s passed
jdivPulloutMinusDenom data()[35] 2.996s passed
jdiv_uniquePosPos data()[36] 2.968s passed
jdiv_uniquePosNeg data()[37] 2.980s passed
jdiv_uniqueNegPos data()[38] 2.954s passed
jdiv_uniqueNegNeg data()[39] 2.973s passed
irrflConcrete1 data()[3] 3.210s passed
jdivMultDenom1 data()[40] 2.994s passed
jdivMultDenom2 data()[41] 2.971s passed
mod_geZero data()[42] 2.949s passed
mod_lessDenom data()[43] 2.946s passed
jmod_NumPos data()[44] 2.928s passed
jmod_NumNeg data()[45] 2.947s passed
jmod_geZero data()[46] 2.945s passed
jmodNumZero data()[47] 2.993s passed
jmod_pulloutminusNum data()[48] 2.956s passed
jmod_pulloutminusDenom data()[49] 2.933s passed
irrflConcrete2 data()[4] 3.118s passed
jmodUnique1 data()[50] 2.996s passed
jmodUnique2 data()[51] 3.007s passed
intDivRem data()[52] 2.933s passed
jmodjmod data()[53] 2.987s passed
jmodDivisible data()[54] 2.983s passed
jmodDivisibleRep data()[55] 2.946s passed
jdivAddMultDenom data()[56] 3.074s passed
jmodAltZero data()[57] 2.947s passed
jmodAddMultDenomZero data()[58] 2.943s passed
polyDiv_zero data()[59] 2.956s passed
cancel_gtPos data()[5] 3.136s passed
polyMod_ltdivDenom data()[60] 2.929s passed
bsum_empty data()[61] 2.922s passed
bsum_induction_upper data()[62] 2.979s passed
bsum_induction_lower data()[63] 2.948s passed
bsum_num_of_bounds data()[64] 2.964s passed
bsum_num_of_bounds2 data()[65] 2.942s passed
bsum_induction_upper2 data()[66] 2.945s passed
bsum_induction_upper_concrete data()[67] 2.947s passed
bsum_induction_upper_concrete_2 data()[68] 2.923s passed
bsum_induction_upper2_concrete data()[69] 2.918s passed
cancel_gtNeg data()[6] 3.051s passed
bsum_induction_lower_concrete data()[70] 2.935s passed
bsum_induction_lower2 data()[71] 2.926s passed
bsum_induction_lower2_concrete data()[72] 2.921s passed
bsum_positive data()[73] 2.980s passed
bsum_upper_bound data()[74] 2.964s passed
bsum_lower_bound data()[75] 2.960s passed
bsum_positive_lower_bound_element data()[76] 2.980s passed
bsum_sub_same_index data()[77] 2.960s passed
bsum_less_same_index data()[78] 3.006s passed
bsum_equal_except_one_index data()[79] 2.962s passed
moduloIntIsInInt data()[7] 3.137s passed
bsum_num_of_is_max data()[80] 2.936s passed
bsum_num_of_is_max2 data()[81] 2.949s passed
bsum_num_of_is_max3 data()[82] 2.982s passed
bsum_num_of_is_max4 data()[83] 2.954s passed
bsum_num_of_lt_max data()[84] 2.949s passed
bsum_num_of_lt_max2 data()[85] 2.946s passed
bsum_num_of_lt_max3 data()[86] 2.968s passed
bsum_num_of_lt_max4 data()[87] 2.951s passed
bsum_num_of_gt0 data()[88] 2.948s passed
bsum_num_of_gt0_alt data()[89] 2.946s passed
moduloLongIsInLong data()[8] 3.052s passed
bsum_add_concrete data()[90] 2.938s passed
bprod_all_positive data()[91] 2.943s passed
bprod_split data()[92] 2.927s passed
powConcrete0 data()[93] 2.943s passed
powConcrete1 data()[94] 2.920s passed
powSplitFactor data()[95] 2.926s passed
powAdd data()[96] 2.939s passed
powMono data()[97] 2.931s passed
powMonoConcrete data()[98] 2.930s passed
powMonoConcreteRight data()[99] 2.925s passed
moduloShortIsInShort data()[9] 3.019s passed

Standard output

352        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
373        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.17ms 
558        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570        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)

1445       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1449       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1454       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1454       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2984       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7804       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.25s 
7885       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7919       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.5ns 
7931       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7932       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.28ms 
7938       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
10640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11531      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms 
11546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.8ns 
11548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
14015      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14815      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
14818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.6ns 
14820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17222      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
17222      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
18028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.7ns 
18030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
20392      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21143      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
21146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21146      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.8ns 
21147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
23499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24279      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.18ms 
24283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 489.8ns 
24285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26582      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
26583      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.71ms 
27333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.9ns 
27335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
29694      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30469      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
30471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.66ms 
30480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
32774      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33522      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.9ns 
33523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.4ns 
33524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
35786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
36537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
36540      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.2ns 
36545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
36546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.2ns 
36547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
38784      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39541      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.7ns 
39542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
39543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
41779      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 507.6ns 
42523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.8ns 
42525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
44762      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
45548      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.66ms 
45549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
45549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
45550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47804      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
47804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
48519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
48557      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.46ms 
48559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
48559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
48561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
50808      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
51521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
51760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 228.48ms 
51763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
51763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
51764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
54025      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
54772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
54778      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
54781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
54781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 769.2ns 
54783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
57019      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
57762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
57765      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
57769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
57769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.3ns 
57770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
60006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
60748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
60808      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.75ms 
60812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
60813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.6ns 
60814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
63040      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
63774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
63790      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
63792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
63792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.6ns 
63793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
66011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
66743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
66763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
66764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
66764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
66770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
68999      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
69729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
69744      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
69746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
69746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.6ns 
69747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
71998      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
72708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
72723      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
72725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
72725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.6ns 
72726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
74953      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
75662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
75686      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.63ms 
75687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
75687      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
75688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77938      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
77938      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
78670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
78673      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
78674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
78674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
78675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80894      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
80894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
81630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
81669      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.82ms 
81671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
81671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.4ns 
81673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
83901      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
84632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
84682      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.73ms 
84685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
84685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299ns 
84686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86911      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
86912      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
87645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
87683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.26ms 
87684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
87684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.4ns 
87685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89899      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
89900      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
90627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
90634      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
90635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
90635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
90636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
92859      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
93571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
93588      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
93590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
93591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 703.9ns 
93592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
95845      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
96561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
96570      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
96571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
96572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
96572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
98813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
99522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
99529      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
99530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
99530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
99531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
101761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
102489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
102496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
102497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
102497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
102498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
104714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
105441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
105448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
105449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
105449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
105450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
107675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
108409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
108412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
108414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
108414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.3ns 
108415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
110628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
111358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
111374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ms 
111376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
111377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.8ns 
111378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
113593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
114326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
114370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.14ms 
114373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
114373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.5ns 
114374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
116615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
117322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
117338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ms 
117340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
117341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 
117341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
119591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
120304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
120319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
120320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
120320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
120321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
122544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
123257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
123272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.39ms 
123273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
123274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
123274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
125503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
126231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
126246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms 
126247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
126247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
126248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
128467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
129200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
129238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.26ms 
129243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
129244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.05ms 
129245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
131486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
132210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
132212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.6ns 
132213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
132213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
132214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
134421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
135158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
135162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
135163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
135163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
135164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
137378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
138102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
138109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
138110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
138110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
138111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
140325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
141029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
141037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
141038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
141038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
141039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
143264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
143968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
143985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.09ms 
143986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
143986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
143987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
146209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
146922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
146929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
146931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
146931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
146931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
149164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
149914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
149922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
149925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
149928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.67ms 
149929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
152149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
152874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
152878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
152879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
152880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
152880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
155082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
155808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
155811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
155813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
155813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
155814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
158016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
158741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
158807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.49ms 
158809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
158809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.5ns 
158810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
161011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
161738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
161814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.05ms 
161816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
161816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
161817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
164043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
164746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
164749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
164750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
164750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
164751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
166980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
167686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
167735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.23ms 
167738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
167742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.62ms 
167743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
169957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
170691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
170718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.35ms 
170721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
170721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.4ns 
170722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
172932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
173661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
173665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
173666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
173666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
173667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
175889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
176614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
176738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.43ms 
176739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
176739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
176740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
178948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
179676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
179686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 
179687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
179687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
179688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
181885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
182615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
182628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
182629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
182629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
182630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
184826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
185570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
185584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
185586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
185586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
185586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
187799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
188502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
188513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
188514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
188514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
188515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
190725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
191433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
191436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
191437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
191437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
191438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
193685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
194412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
194416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
194417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
194417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
194418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
196618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
197342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
197364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ms 
197365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
197365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
197366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
199577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
200310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
200325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
200329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
200329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
200330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
202522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
203254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
203269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ms 
203271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
203271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219ns 
203272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
205481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
206211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
206214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
206216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
206216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197ns 
206217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
208418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
209158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
209162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
209163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
209163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
209164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
211377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
212080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
212085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
212086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
212086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
212087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
214297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
215000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
215003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
215004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
215005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
215005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
217211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
217935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
217937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686ns 
217939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
217939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
217939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
220138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
220861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
220864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
220865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
220865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
220866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
223061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
223783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
223785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.1ns 
223786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
223786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
223787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
225985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
226708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
226763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.99ms 
226767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
226767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
226768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
228966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
229688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
229729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.07ms 
229730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
229730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
229731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
231926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
232650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
232689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.59ms 
232691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
232691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
232691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
234911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
235614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
235670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.96ms 
235671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
235671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
235672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
237898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
238602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
238630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.83ms 
238631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
238631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
238632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
240850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
241588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
241636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.18ms 
241637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
241637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
241638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
243850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
244574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
244598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.01ms 
244600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
244600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
244600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
246794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
247517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
247535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.17ms 
247536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
247536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
247537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
249731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
250460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
250483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
250485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
250485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.5ns 
250486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
252710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
253447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
253465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
253466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
253467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
253467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
255666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
256394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
256419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
256421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
256421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.5ns 
256422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
258639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
259345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
259368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.14ms 
259370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
259370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
259370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
261588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
262293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
262315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.06ms 
262316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
262316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
262317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
264535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
265260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
265282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.98ms 
265284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
265284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208ns 
265285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
267488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
268215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
268234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.13ms 
268235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
268235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
268235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
270435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
271159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
271181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.06ms 
271182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
271182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
271183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
273380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
274105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
274128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ms 
274129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
274129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
274130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
276333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
277058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
277065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
277066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
277066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
277067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
279281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
279992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
280008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
280010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
280010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
280010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
282226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
282932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
282936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
282937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
282937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
282937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
285147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
285877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
285879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 517.9ns 
285881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
285881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157ns 
285882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
288073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
288797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
288800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.3ns 
288801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
288801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
288801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
290990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
291715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
291722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
291728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
291728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
291728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
293932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
294660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
294665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
294667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
294667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
294668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
296860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
297585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
297597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
297598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
297598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
297598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
299797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
300523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
300526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
300527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
300527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
300528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
302743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
303449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
303451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.4ns 
303453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
303453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
303453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
305660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
306365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
306369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
306370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
306370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
306371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
308585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
309289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
309291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 500ns 
309292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
309292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
309293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
311504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
312228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
312229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.3ns 
312231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
312231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
312231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
314427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
315152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
315154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.8ns 
315155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
315155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
315156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
317351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
318076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
318080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
318081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
318081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
318081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
320265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
320988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
320997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
320998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
320998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
320998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
323188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
323911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
323915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
323916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
323916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
323917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
326115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
326846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
326852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
326853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
326853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
326854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
329064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
329771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
329778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
329780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
329781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
329783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
331998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
332702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
332716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
332718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
332718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
332718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
334924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
335649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
335652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
335653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
335653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
335653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
337848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
338573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
338575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
338576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
338577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
338577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
340774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
341501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
341504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
341505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
341505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
341506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
343696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
344421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
344436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.83ms 
344438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
344438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
344438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
346631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
347360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
347364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.1ns 
347366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
347366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
347366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
349555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
350276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
350310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.03ms 
350311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
350312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
350312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
352516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
353220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
353223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
353224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
353224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
353225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
355438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
356144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
356163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ms 
356164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
356164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
356165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
358390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
359115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
359133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
359134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
359134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
359135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
361324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
362050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
362071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms 
362072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
362073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
362073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
364276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
365005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
365007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.9ns 
365009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
365009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 
365010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
367226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
367962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
367967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
367968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
367968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
367969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
370160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
370886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
370889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
370890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
370890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
370891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
373107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
373814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
373816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.8ns 
373818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
373818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
373818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
376033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
376741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
376743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685ns 
376744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
376744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
376745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
378956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
379687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
379690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
379694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
379694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.4ns 
379695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
381892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
382620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
382623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
382624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
382624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
382625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
384818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
385548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
385557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ms 
385559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
385559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
385559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
387772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
388482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
388495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
388496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
388496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
388497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
390700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
391409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
391420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.65ms 
391421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
391422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
391422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
393630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
394367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
394386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
394387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
394387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
394388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
396586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
397322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
397326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
397327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
397327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
397328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
399516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
400250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
400256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
400257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
400257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
400258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
402462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
403178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
403180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720ns 
403181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
403181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
403182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
405389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
406127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
406129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
406130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
406131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
406131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
408321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
409058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
409060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 857.8ns 
409061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
409061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
409062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
411266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
411984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
411994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
411995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
411996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
411996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
414221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
414960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
414964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
414965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
414965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
414966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
417157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
417894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
417900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
417901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
417902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
417902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
420091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
420827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
420829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.1ns 
420830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
420830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
420831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
423046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
423783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
423785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.4ns 
423786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
423786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
423787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
425982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
426719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
426722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
426723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
426723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
426724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
428917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
429652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
429655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
429656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
429656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
429656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
431859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
432597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
432600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
432601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
432601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
432602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
434793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
435532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
435534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
435535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
435535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
435536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
437744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
438461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
438465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
438466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
438466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
438467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
440674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
441410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
441412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
441414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
441414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
441414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
443607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
444342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
444352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
444353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
444353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
444354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
446564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
447282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
447284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665ns 
447285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
447285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
447286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
449492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
450229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
450235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
450236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
450236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
450237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
452444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
453160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
453162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.9ns 
453163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
453163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
453163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
455369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
456105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
456107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.2ns 
456108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
456108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
456109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
458296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
459033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
459037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
459038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
459038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
459039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
461247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
461998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
462001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
462002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
462002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
462003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
464265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
465025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
465028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
465030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
465030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
465030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
467274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
468009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
468013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
468014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
468014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
468015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
470207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
470944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
470949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
470951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
470951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.5ns 
470952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
473153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
473887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
473900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
473901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
473901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
473902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
476094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
476827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
476841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
476842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
476842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
476843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
479045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
479779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
479789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
479790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
479790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
479790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
481992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
482730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
482740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
482741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
482741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
482742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
484954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
485689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
485712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.47ms 
485714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
485714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
485714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
487906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
488642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
488665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
488666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
488666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
488667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
490880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
491616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
491637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.58ms 
491639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
491639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
491639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
493851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
494566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
494579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
494580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
494581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
494581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
496783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
497516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
497543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.53ms 
497544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
497545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
497545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
499752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
500490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
500533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.94ms 
500535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
500535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
500535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
502724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
503458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
503492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.09ms 
503493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
503493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
503494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
505701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
506446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
506484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.06ms 
506485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
506485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
506486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
508697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
509432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
509472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.26ms 
509473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
509473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
509474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
511662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
512395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
512507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.29ms 
512509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
512509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
512509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
514713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
515449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
515456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
515457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
515457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
515458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
517657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
518395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
518402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
518404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
518404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200ns 
518404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
520596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
521333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
521337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
521338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
521338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
521339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
523546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
524281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
524298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
524299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
524299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
524300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
526505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
527240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
527250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
527251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
527251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.3ns 
527251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
529462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
530178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
530182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
530183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
530183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
530183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
532386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
533143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
533159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.87ms 
533160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
533160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
533161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
535441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
536202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
536218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
536219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
536219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
536220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
538499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
539260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
539278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.62ms 
539280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
539280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
539280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
541558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
542298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
542301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
542302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
542302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
542303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
544565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
545301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
545305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
545306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
545306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
545306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
547510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
548246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
548251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
548252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
548253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
548253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
550461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
551207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
551213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
551214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
551214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
551214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
553423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
554160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
554225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.19ms 
554227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
554227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
554227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
556437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
557178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
557204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.23ms 
557209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
557209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.1ns 
557210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
559392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
560125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
560145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.28ms 
560147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
560147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
560147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
562352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
563087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
563089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 273.7ns 
563090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
563090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
563091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
565314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
566051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
566239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.93ms 
566242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
566242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.7ns 
566243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
568496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
569249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
569297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.86ms 
569299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
569299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.5ns 
569300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
571509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
572246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
572248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.1ns 
572249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
572249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
572250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
574451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
575188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
575189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 309.2ns 
575191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
575191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
575191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
577392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
578128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
578130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305ns 
578131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
578131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
578132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
580334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
581070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
581071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438ns 
581073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
581073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
581073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
583277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
584014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
584097     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
584109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.97ms 
584111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
584111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
584114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
586334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
587069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
587119     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
587119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.93ms 
587120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
587120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
587122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
589341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
590078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
590080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
590104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
590139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
590165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
590173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
590184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
590187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
590188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
590190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
590195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
590197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
590201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
590202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
590424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
590426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
590428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
590428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
590429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
590556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
590557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
590558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
590559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
590560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
590561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
590718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
590719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
590721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
590721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
590723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
590726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
590831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
590833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
590834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
590835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
590836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
590837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
590844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
590845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
590845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
590848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
590852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
590853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
590860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
590862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
590863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
590863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
590865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
590866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
590972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
590974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
590976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
591072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
591073     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)'' 
591076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
591077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
591078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
591079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
591080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
591082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
591085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
591086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
591087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
591088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
591089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
591175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
591178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
591179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
591180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
591181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
591182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
591183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
591287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
591288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
591289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
591291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
591292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
591292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
591293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
591295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
591373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
591375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
591445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
591449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
591454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
591455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
591458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
591460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
591460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
591461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
591461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
591463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
591472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
591479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
591580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
591583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
591585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
591586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
591587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
591587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
591588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
591589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
591636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
591640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
591719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
591720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
591722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
591724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
591724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
591725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
591832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
591836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
591838     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)'' 
591840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
591842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
591843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
591844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
591845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
591854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
591859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
591861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
591861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
591940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
591941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
591942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
591943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
591943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
591944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
592038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
592040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
592041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
592042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
592043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
592043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
592044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
592045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
592117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
592118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
592185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
592186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
592186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
592190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
592194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
592198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
592342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
592344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
592344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
592345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
592354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
592427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
595707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
595708     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)'' 
595713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
595714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
595715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
595715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
595716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
595723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
595724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
595726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
595726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
595727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
595814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
595817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
595818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
595819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
595819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
595820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
595821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
595911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
595913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
595914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
595915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
595915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
595916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
595916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
595917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
595988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
595989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
596057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
596061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
596065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
596066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
596066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
596067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
596076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
596151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
596152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
596153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
596154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
596261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
596269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
596270     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)'' 
596272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
596273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
596274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
596274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
596275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
596284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
596286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
596287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
596287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
596288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
596370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
596371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
596373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
596373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
596374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
596459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
596463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
596464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
596464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
596465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
596466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
596466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
596558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
596559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
596560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
596561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
596561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
596562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
596562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
596563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
596564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
596564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
596565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
596566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
596566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
596566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
596567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
596648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
596649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
596654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
596726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
596800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
596801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
596802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
596803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
596803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
596804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
596804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
596804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
596805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
596884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
596889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
596972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
596973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
596974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
596974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
596975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
596975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
596975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
596976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
596980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
596981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
597054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
597058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
597063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
597155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
597156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
597157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
597157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
597158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
597158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
597158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
597159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
597209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
597210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
597211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
597211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
597212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
597220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
597224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
597333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
597415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
597416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
597416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
597417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
597575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
597658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
597659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
600506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
600511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
600512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
600513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
600513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
600620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
600621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
600622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
600623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
600624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
600722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
603512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
606504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
606509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
606510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
606510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
606511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
606617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
606618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
606619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
606620     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)' ...' 
606621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
607660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
607660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
607661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
609968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
610721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
610722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
610723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
610742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
610759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
610761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
610763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
610763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
610767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
610769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
610771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
610774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
610774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
610782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
610784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
610785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
610834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
610835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
610835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
610836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
610836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
610903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
610903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
610905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
610905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
610906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
610909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
610909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
610909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
610910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
610911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
610912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
610997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
610997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
610998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
610999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
611000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
611000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
611096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
611096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
611097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
611097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
611098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
611099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
611099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
611099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
611100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
611100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
611100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
611101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
611101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
611101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
611102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
611102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
611102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
611103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
611104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
611106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
611144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
611145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
611209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
611210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
611211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
611212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
611213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
611213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
611269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
611271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
611272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
611273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
611274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
611275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
611275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
611332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
611334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
611337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
611405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
611466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
611466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
611466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
613736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
614522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
614550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.72ms