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

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

tests
0

failures
0

ignored
13m36.29s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.968s passed
powPositiveConcrete data()[101] 3.877s passed
powGeq1Concrete data()[102] 3.865s passed
pow2InIntLower data()[103] 4.000s passed
pow2InIntUpper data()[104] 3.873s passed
logSelfConcrete data()[105] 3.878s passed
log1Concrete data()[106] 3.888s passed
logProduct data()[107] 3.914s passed
logTimesBaseConcrete data()[108] 3.874s passed
logProdIdentity data()[109] 3.941s passed
moduloByteIsInByte data()[10] 4.325s passed
logProdIdentityConcrete data()[110] 3.907s passed
logPowIdentity data()[111] 3.913s passed
logPowIdentityConcrete data()[112] 3.945s passed
logPositive data()[113] 3.893s passed
logPositiveConcrete data()[114] 3.826s passed
logMono data()[115] 3.969s passed
logMonoConcrete data()[116] 3.958s passed
powLogLess data()[117] 3.903s passed
powLogMore2 data()[118] 3.869s passed
logLessThanPow data()[119] 3.888s passed
moduloCharIsInChar data()[11] 4.290s passed
logLessThanPowConcrete data()[120] 3.858s passed
logSqueeze data()[121] 3.918s passed
ifthenelse_equals data()[122] 3.943s passed
ifthenelse_equals_1 data()[123] 3.887s passed
ifthenelse_equals_2 data()[124] 3.867s passed
disjointWithSingleton1 data()[125] 3.859s passed
disjointWithSingleton2 data()[126] 3.827s passed
disjointArrayRanges data()[127] 3.796s passed
disjointArrayRangeAllFields1 data()[128] 3.920s passed
disjointArrayRangeAllFields2 data()[129] 3.860s passed
div_unique1 data()[12] 4.240s passed
seqSelfDefinition data()[130] 3.942s passed
seqOutsideValue data()[131] 3.959s passed
castedGetAny data()[132] 3.933s passed
seqGetAlphaCast data()[133] 3.854s passed
getOfSeqSingleton data()[134] 3.972s passed
getOfSeqSingletonConcrete data()[135] 4.050s passed
getOfSeqConcat data()[136] 4.005s passed
getOfSeqSub data()[137] 4.009s passed
getOfSeqReverse data()[138] 3.962s passed
lenOfSeqEmpty data()[139] 3.963s passed
div_unique2 data()[13] 4.109s passed
lenOfSeqSingleton data()[140] 3.941s passed
lenOfSeqConcat data()[141] 3.961s passed
lenOfSeqSub data()[142] 3.915s passed
lenOfSeqReverse data()[143] 3.903s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.928s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.910s passed
getOfSeqSingletonEQ data()[146] 3.923s passed
getOfSeqConcatEQ data()[147] 3.886s passed
getOfSeqSubEQ data()[148] 3.948s passed
getOfSeqReverseEQ data()[149] 3.869s passed
div_exists data()[14] 4.340s passed
lenOfSeqEmptyEQ data()[150] 3.972s passed
lenOfSeqSingletonEQ data()[151] 3.848s passed
lenOfSeqConcatEQ data()[152] 3.917s passed
lenOfSeqSubEQ data()[153] 3.905s passed
lenOfSeqReverseEQ data()[154] 3.829s passed
getOfSeqDefEQ data()[155] 3.967s passed
lenOfSeqDefEQ data()[156] 3.930s passed
seqConcatWithSeqEmpty1 data()[157] 3.943s passed
seqConcatWithSeqEmpty2 data()[158] 3.830s passed
seqReverseOfSeqEmpty data()[159] 4.099s passed
div_one data()[15] 4.113s passed
subSeqComplete data()[160] 3.920s passed
subSeqTailR data()[161] 4.097s passed
subSeqTailL data()[162] 4.059s passed
subSeqTailEQR data()[163] 3.937s passed
subSeqTailEQL data()[164] 3.937s passed
seqDef_split data()[165] 3.966s passed
seqDef_induction_upper data()[166] 3.990s passed
seqDef_induction_upper_concrete data()[167] 4.062s passed
seqDef_induction_lower data()[168] 3.986s passed
seqDef_induction_lower_concrete data()[169] 3.947s passed
jdiv_one data()[16] 4.126s passed
seqDef_split_in_three data()[170] 4.024s passed
seqDef_empty data()[171] 3.920s passed
seqDef_one_summand data()[172] 3.856s passed
seqDef_lower_equals_upper data()[173] 3.861s passed
seqDefOfSeq data()[174] 3.887s passed
seqSelfDefinitionEQ2 data()[175] 3.889s passed
indexOfSeqSingleton data()[176] 3.912s passed
indexOfSeqConcatFirst data()[177] 3.971s passed
indexOfSeqConcatSecond data()[178] 3.981s passed
indexOfSeqSub data()[179] 3.985s passed
div_zero data()[17] 4.178s passed
lenOfArray2seq data()[180] 4.033s passed
getAnyOfArray2seq data()[181] 3.975s passed
getOfArray2seq data()[182] 3.931s passed
getAnyOfNPermInv data()[183] 3.922s passed
seqNPermRange data()[184] 4.014s passed
seqPermTrans data()[185] 4.018s passed
seqPermRefl data()[186] 3.996s passed
seqPermSplit data()[187] 4.014s passed
seqNPermRight data()[188] 4.323s passed
seqPermFromSwap data()[189] 4.027s passed
divResZero1 data()[18] 4.074s passed
seqPermTransAlt0 data()[190] 3.861s passed
seqPermTransAlt1 data()[191] 3.952s passed
seqPermTransAlt2 data()[192] 3.954s passed
seqPermTransAlt3 data()[193] 3.842s passed
seqPermForall data()[194] 4.073s passed
seqPermExists data()[195] 4.019s passed
schiffl_lemma_2 data()[196] 29.225s passed
schiffl_thm_1 data()[197] 4.840s passed
eqSameSeq data()[198] 4.145s passed
divResZero2 data()[19] 4.034s passed
eqTermCut data()[1] 5.339s passed
divResOne1 data()[20] 4.103s passed
divResOne2 data()[21] 4.173s passed
div_cancel1 data()[22] 4.182s passed
div_cancel2 data()[23] 4.051s passed
divAddMultDenom data()[24] 4.216s passed
divMinus data()[25] 4.180s passed
divMinusDenom data()[26] 4.117s passed
divLeastDPos data()[27] 4.127s passed
divLeastDNeg data()[28] 4.157s passed
divGreatestDPos data()[29] 4.158s passed
equivAllRight data()[2] 4.687s passed
divGreatestDNeg data()[30] 4.083s passed
divIncreasingPos data()[31] 4.021s passed
divIncreasingNeg data()[32] 4.037s passed
jdiv_zero data()[33] 4.026s passed
jdivPulloutMinusNum data()[34] 3.974s passed
jdivPulloutMinusDenom data()[35] 4.075s passed
jdiv_uniquePosPos data()[36] 3.999s passed
jdiv_uniquePosNeg data()[37] 4.040s passed
jdiv_uniqueNegPos data()[38] 3.927s passed
jdiv_uniqueNegNeg data()[39] 3.953s passed
irrflConcrete1 data()[3] 4.464s passed
jdivMultDenom1 data()[40] 3.906s passed
jdivMultDenom2 data()[41] 3.911s passed
mod_geZero data()[42] 3.926s passed
mod_lessDenom data()[43] 3.892s passed
jmod_NumPos data()[44] 3.893s passed
jmod_NumNeg data()[45] 3.988s passed
jmod_geZero data()[46] 3.936s passed
jmodNumZero data()[47] 3.865s passed
jmod_pulloutminusNum data()[48] 3.918s passed
jmod_pulloutminusDenom data()[49] 3.957s passed
irrflConcrete2 data()[4] 4.373s passed
jmodUnique1 data()[50] 3.986s passed
jmodUnique2 data()[51] 4.041s passed
intDivRem data()[52] 3.910s passed
jmodjmod data()[53] 4.038s passed
jmodDivisible data()[54] 4.036s passed
jmodDivisibleRep data()[55] 3.999s passed
jdivAddMultDenom data()[56] 4.244s passed
jmodAltZero data()[57] 4.273s passed
jmodAddMultDenomZero data()[58] 3.880s passed
polyDiv_zero data()[59] 3.899s passed
cancel_gtPos data()[5] 4.349s passed
polyMod_ltdivDenom data()[60] 3.900s passed
bsum_empty data()[61] 3.921s passed
bsum_induction_upper data()[62] 3.851s passed
bsum_induction_lower data()[63] 3.916s passed
bsum_num_of_bounds data()[64] 3.888s passed
bsum_num_of_bounds2 data()[65] 3.938s passed
bsum_induction_upper2 data()[66] 3.845s passed
bsum_induction_upper_concrete data()[67] 3.990s passed
bsum_induction_upper_concrete_2 data()[68] 3.927s passed
bsum_induction_upper2_concrete data()[69] 3.908s passed
cancel_gtNeg data()[6] 4.170s passed
bsum_induction_lower_concrete data()[70] 3.951s passed
bsum_induction_lower2 data()[71] 3.924s passed
bsum_induction_lower2_concrete data()[72] 3.905s passed
bsum_positive data()[73] 3.929s passed
bsum_upper_bound data()[74] 4.005s passed
bsum_lower_bound data()[75] 3.940s passed
bsum_positive_lower_bound_element data()[76] 3.969s passed
bsum_sub_same_index data()[77] 3.879s passed
bsum_less_same_index data()[78] 4.006s passed
bsum_equal_except_one_index data()[79] 3.916s passed
moduloIntIsInInt data()[7] 4.223s passed
bsum_num_of_is_max data()[80] 4.003s passed
bsum_num_of_is_max2 data()[81] 3.951s passed
bsum_num_of_is_max3 data()[82] 4.030s passed
bsum_num_of_is_max4 data()[83] 4.062s passed
bsum_num_of_lt_max data()[84] 4.102s passed
bsum_num_of_lt_max2 data()[85] 3.976s passed
bsum_num_of_lt_max3 data()[86] 3.964s passed
bsum_num_of_lt_max4 data()[87] 3.903s passed
bsum_num_of_gt0 data()[88] 3.908s passed
bsum_num_of_gt0_alt data()[89] 3.884s passed
moduloLongIsInLong data()[8] 4.158s passed
bsum_add_concrete data()[90] 3.899s passed
bprod_all_positive data()[91] 3.925s passed
bprod_split data()[92] 3.904s passed
powConcrete0 data()[93] 3.849s passed
powConcrete1 data()[94] 3.898s passed
powSplitFactor data()[95] 3.827s passed
powAdd data()[96] 3.861s passed
powMono data()[97] 3.893s passed
powMonoConcrete data()[98] 3.922s passed
powMonoConcreteRight data()[99] 3.914s passed
moduloShortIsInShort data()[9] 4.109s passed

Standard output

494        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
545        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 16.45ms 
893        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
910        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)

2345       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2349       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2352       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2353       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4243       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11275      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.38s 
11389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11440      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37ns 
11461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 732ns 
11468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 
15453      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16787      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.25ms 
16799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.8ns 
16801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
20324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21484      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms 
21489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.7ns 
21493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
24897      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25950      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
25954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.2ns 
25956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
29198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30325      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
30328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms 
30330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
33579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34673      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.61ms 
34681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34682      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 535.1ns 
34683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
37793      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38845      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.87ms 
38850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.2ns 
38852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
42080      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43071      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
43074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.1ns 
43076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
46214      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.5ns 
47233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.4ns 
47235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50318      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
50318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
51338      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.68ns 
51341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
51342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.29ns 
51344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
54612      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55665      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.5ns 
55668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 524.7ns 
55670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
58933      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
59954      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
59959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
59960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 538.7ns 
59961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
63142      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64196      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.96ms 
64204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
64205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 597.6ns 
64206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
67286      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
68257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
68309      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.08ms 
68312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
68312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.4ns 
68314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
71401      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
72415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
72648      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 220.13ms 
72652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
72652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.6ns 
72654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
75786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
76756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
76763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
76766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
76766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.7ns 
76768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
79865      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
80882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
80889      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
80892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
80893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.3ns 
80894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
83969      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
85066      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.5ms 
85071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
85072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.3ns 
85073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
88133      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
89110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
89144      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.31ms 
89148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
89149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.8ns 
89151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
92198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
93153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
93178      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.12ms 
93182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
93182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.7ns 
93184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96253      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
96254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
97254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
97281      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
97285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
97285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337ns 
97286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
100393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
101432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
101455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19ms 
101458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
101458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.5ns 
101460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
104607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
105600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
105637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.21ms 
105639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
105639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
105641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
108722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
109684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
109688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
109691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
109692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 509.6ns 
109694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
112796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
113784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
113904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.95ms 
113907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
113907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.9ns 
113909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
116983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
117983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
118083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.25ms 
118086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
118087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.5ns 
118088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
121145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
122120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
122200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.04ms 
122205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
122206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 777.2ns 
122208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
125306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
126302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
126330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.24ms 
126332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
126333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.7ns 
126334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
129452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
130467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
130487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
130489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
130489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
130490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
133627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
134622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
134644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
134647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
134647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
134648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
137751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
138728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
138730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
138730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 
138731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
141755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
142738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
142749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
142751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
142751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.5ns 
142752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
145821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
146775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
146785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
146788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
146788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
146789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
149848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
150806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
150812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
150814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
150814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
150815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
153800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
154770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
154786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.38ms 
154788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
154788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.8ns 
154789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
157788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
158755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
158860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.73ms 
158864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
158864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.2ns 
158865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
161883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
162832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
162860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.72ms 
162863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
162863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.9ns 
162865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
165912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
166872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
166900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.12ms 
166902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
166903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
166904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
169825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
170790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
170828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.22ms 
170830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
170830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
170831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
173751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
174750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
174780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.61ms 
174783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
174783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301ns 
174785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
177707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
178627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
178687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.08ms 
178689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
178689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
178690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
181641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
182590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
182594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
182601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
182601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.3ns 
182604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
185539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
186502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
186522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
186527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
186529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.12ms 
186530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
189464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
190407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
190418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
190420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
190420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
190421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
193364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
194293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
194310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.75ms 
194313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
194314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.8ns 
194320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
197279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
198271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
198299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
198301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
198301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
198302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
201261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
202224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
202235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.02ms 
202237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
202237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
202238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
205119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
206095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
206100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
206102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
206103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 
206104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
209092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
210014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
210018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
210020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
210020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
210021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
213026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
213968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
213974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
213977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
213977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
213978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
216900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
217838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
217960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.09ms 
217963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
217964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 
217965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
220906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
221873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
222001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.13ms 
222004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
222004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.8ns 
222006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
224985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
225907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
225912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
225914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
225914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
225915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
228898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
229875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
229948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.18ms 
229952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
229954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.77ms 
229955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
232925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
233940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
233986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.36ms 
233988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
233988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.5ns 
233989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
237007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
237981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
237985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
237987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
237987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
237988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
241011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
241963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
242228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 250ms 
242235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
242235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.3ns 
242236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
245492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
246483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
246502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.81ms 
246505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
246505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.3ns 
246508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
249402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
250369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
250382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
250384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
250384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
250384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
253319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
254257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
254281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.68ms 
254283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
254283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
254284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
257230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
258155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
258180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
258183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
258183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
258184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
261146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
262096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
262102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
262104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
262104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
262105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
264978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
265946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
265953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
265955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
265955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
265956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
268870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
269832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
269869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.04ms 
269871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
269871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
269872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
272797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
273726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
273757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.32ms 
273759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
273759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
273760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
276710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
277638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
277695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.61ms 
277696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
277697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
277697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
280575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
281530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
281539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
281542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
281542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.4ns 
281543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
284569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
285523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
285530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
285532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
285532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
285533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
288506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
289449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
289457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
289458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
289458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
289459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
292423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
293362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
293366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
293367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
293367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
293368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
296378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
297312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
297315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
297318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
297318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
297319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
300256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
301234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
301240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
301242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
301242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
301243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
304196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
305141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
305145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
305147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
305147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 
305148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
308080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
308999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
309074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.38ms 
309076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
309077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.8ns 
309078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
312081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
313012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
313079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.71ms 
313081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
313081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.9ns 
313082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
315997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
316973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
317019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.12ms 
317021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
317021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
317022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
319967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
320921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
320988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.84ms 
320989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
320989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
320990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
323924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
324821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
324867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.91ms 
324869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
324869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
324870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
327844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
328789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
328872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.74ms 
328875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
328875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.9ns 
328876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
331793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
332746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
332789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.67ms 
332791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
332791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.8ns 
332792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
335792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
336763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
336792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.24ms 
336794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
336794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
336795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
339787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
340702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
340743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.29ms 
340745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
340746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns 
340747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
343782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
344744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
344773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.84ms 
344775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
344776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.6ns 
344777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
347799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
348789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
348835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.67ms 
348836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
348836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
348837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
351903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
352895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
352937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.63ms 
352939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
352939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
352940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
355971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
356873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
356913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.66ms 
356915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
356915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
356916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
359890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
360837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
360877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.21ms 
360878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
360878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
360879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
363772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
364746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
364779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.7ms 
364782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
364782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
364783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
367712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
368649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
368688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.89ms 
368691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
368691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 597.3ns 
368692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
371608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
372528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
372572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.99ms 
372574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
372574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
372575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
375504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
376460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
376471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
376473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
376473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
376474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
379441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
380368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
380396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms 
380398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
380398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
380398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
383346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
384294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
384301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
384302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
384302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.5ns 
384303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
387238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
388146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
388149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
388151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
388151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
388152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
391095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
392044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
392047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.3ns 
392048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
392048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
392049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
394937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
395863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
395874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
395876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
395876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
395877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
398770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
399727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
399736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
399737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
399737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.4ns 
399738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
402674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
403608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
403628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
403630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
403630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
403631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
406600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
407545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
407550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
407551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
407551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
407552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
410498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
411461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
411464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.1ns 
411465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
411466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns 
411467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
414458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
415425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
415432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
415434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
415434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
415435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
418395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
419307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
419309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.7ns 
419311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
419311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
419312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
422236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
423171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
423174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.8ns 
423175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
423175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
423176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
426197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
427172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
427174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.9ns 
427175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
427176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
427176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
430101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
431042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
431047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
431049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
431049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
431050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
433957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
434911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
434925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
434926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
434927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
434927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
437876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
438808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
438813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
438815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
438815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
438816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
441768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
442717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
442727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
442729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
442729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
442730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
445665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
446594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
446601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
446603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
446603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.7ns 
446604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
449541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
450520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
450542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.11ms 
450544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
450544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
450545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
453514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
454444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
454449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
454450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
454450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
454451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
457413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
458357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
458362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
458363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
458364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
458364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
461354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
462302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
462307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
462309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
462309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
462311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
465218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
466173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
466200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.73ms 
466201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
466201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
466202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
469100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
470019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
470024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.3ns 
470027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
470028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
470028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
472983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
473931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
473995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.05ms 
473997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
473997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 
473998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
476994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
477949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
477953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
477955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
477955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
477955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
480872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
481824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
481856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms 
481858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
481858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
481859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
484750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
485689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
485725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.82ms 
485727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
485728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
485728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
488666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
489571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
489613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.87ms 
489615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
489615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
489616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
492531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
493468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
493472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
493473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
493473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
493474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
496453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
497382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
497390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
497391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
497391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
497392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
500367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
501328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
501332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
501334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
501334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
501335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
504245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
505215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
505219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
505221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
505221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
505221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
508141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
509082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
509086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
509088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
509088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
509088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
511991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
512940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
512945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
512947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
512947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.2ns 
512948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
515842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
516768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
516773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
516774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
516775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
516775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
519627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
520553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
520568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
520570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
520571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.2ns 
520572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
523517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
524471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
524488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
524490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
524490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
524490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
527385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
528333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
528348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
528350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
528350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
528350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
531252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
532259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
532290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.21ms 
532292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
532292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.2ns 
532292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
535275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
536243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
536249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
536250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
536250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
536251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
539204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
540174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
540183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
540184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
540184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
540185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
543085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
544030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
544037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
544039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
544039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
544039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
547060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
548004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
548008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
548010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
548010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
548011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
551078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
552055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
552058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
552059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
552060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
552060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
555088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
556047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
556063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
556065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
556065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
556066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
559076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
560067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
560072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
560074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
560074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
560075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
563069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
564024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
564035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
564036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
564036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
564037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
567021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
567994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
567997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
567999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
567999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
568000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
570990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
571936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
571939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.81ns 
571940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
571940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
571941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
574905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
575894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
575899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
575901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
575901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.3ns 
575902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
578856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
579810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
579814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
579816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
579816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
579817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
582764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
583713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
583717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
583718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
583718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
583719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
586718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
587641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
587645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
587646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
587647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
587647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
590566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
591546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
591555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
591557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
591557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.1ns 
591559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
594493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
595474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
595478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
595480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
595481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
595481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
598393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
599349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
599364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms 
599365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
599365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
599366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
602339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
603309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
603312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.11ns 
603313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
603314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
603314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
606225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
607170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
607181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.51ms 
607183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
607183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
607184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
610202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
611150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
611153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
611155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
611155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
611156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
614052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
614998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
615002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
615003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
615003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
615004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
617942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
618911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
618918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
618919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
618919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
618920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
621870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
622820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
622824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
622825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
622825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
622826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
625692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
626647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
626652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
626654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
626654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
626655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
629654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
630613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
630619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
630621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
630621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
630621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
633557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
634542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
634549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
634550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
634551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
634552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
637522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
638471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
638492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.27ms 
638494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
638494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
638495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
641382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
642301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
642322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
642324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
642324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
642325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
645352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
646407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
646421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.47ms 
646423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
646423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
646424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
649377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
650325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
650341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
650343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
650343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
650344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
653403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
654400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
654438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.09ms 
654440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
654440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
654441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
657477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
658460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
658497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.49ms 
658499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
658499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
658500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
661434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
662400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
662435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.19ms 
662436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
662436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
662437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
665401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
666351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
666371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.12ms 
666373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
666373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
666374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
669349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
670289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
670337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.95ms 
670339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
670339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
670340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
673312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
674253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
674327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.37ms 
674329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
674329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
674330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
677350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
678330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
678389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.32ms 
678391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
678391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
678392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
681344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
682310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
682374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.53ms 
682376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
682376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
682377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
685276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
686257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
686322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.73ms 
686324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
686324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
686325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
689211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
690177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
690345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 159.53ms 
690347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
690347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
690348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
693290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
694250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
694266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ms 
694268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
694268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
694269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
697148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
698111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
698122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
698124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
698124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
698125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
701018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
701975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
701983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
701987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
701987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
701988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
704897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
705846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
705872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.33ms 
705874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
705874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
705875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
708784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
709745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
709761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
709763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
709763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
709764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
712678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
713669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
713673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
713674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
713675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
713675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
716658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
717620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
717645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.47ms 
717646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
717646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
717647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
720611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
721601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
721625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms 
721627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
721627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.7ns 
721628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
724599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
725581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
725610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.85ms 
725612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
725612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
725613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
728663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
729638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
729643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
729645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
729645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 
729646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
732632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
733613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
733619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
733620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
733620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
733621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
736582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
737540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
737549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
737551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
737551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
737551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
740477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
741462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
741472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
741473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
741473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
741474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
744423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
745379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
745485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.99ms 
745487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
745488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.8ns 
745489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
748476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
749461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
749503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.25ms 
749505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
749505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
749506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
752486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
753467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
753499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.75ms 
753501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
753501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
753501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
756514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
757510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
757513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 463.3ns 
757515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
757515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
757516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
760526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
761552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
761836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270.32ms 
761838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
761838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
761840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
764814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
765786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
765864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.57ms 
765866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
765866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
765867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
768755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
769723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
769726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513.1ns 
769727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
769727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
769728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
772683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
773675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
773677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 509.5ns 
773679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
773679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
773679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
776681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
777628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
777631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.6ns 
777633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
777633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
777634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
780519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
781471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
781473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.6ns 
781474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
781474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
781475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
784430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
785384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
785545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 158.85ms 
785549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
785549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 
785550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
788560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
789503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
789564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.23ms 
789566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
789566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
789568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
792598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
793576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
793578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
793616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
793660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
793682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
793687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
793693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
793696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
793697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
793700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
793703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
793705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
793708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
793709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
793948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
793950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
793952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
793953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
793954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
794141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
794143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
794146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
794149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
794151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
794152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
794378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
794382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
794383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
794384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
794385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
794389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
794616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
794619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
794621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
794622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
794623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
794624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
794636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
794638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
794639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
794642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
794643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
794644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
794658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
794660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
794661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
794662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
794663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
794665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
794925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
794926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
794927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
795118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
795119     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)'' 
795122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
795123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
795124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
795126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
795127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
795127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
795132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
795133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
795135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
795135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
795136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
795300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
795305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
795307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
795308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
795308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
795309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
795310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
795469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
795470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
795471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
795473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
795474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
795475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
795475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
795477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
795614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
795616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
795744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
795749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
795755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
795756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
795757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
795759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
795759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
795760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
795760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
795762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
795771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
795776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
795905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
795906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
795907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
795908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
795909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
795909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
795910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
795911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
795978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
795985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
796113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
796114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
796116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
796118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
796119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
796120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
796320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
796326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
796327     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)'' 
796329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
796330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
796331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
796332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
796332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
796345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
796347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
796348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
796349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
796509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
796511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
796512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
796513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
796514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
796515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
796655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
796656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
796658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
796659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
796660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
796662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
796662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
796664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
796774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
796777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
796877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
796878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
796879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
796885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
796890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
796896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
797057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
797058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
797060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
797061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
797074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
797203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
801872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
801873     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)'' 
801881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
801882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
801882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
801883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
801884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
801894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
801896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
801898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
801898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
801899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
802023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
802029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
802030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
802031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
802032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
802033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
802034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
802161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
802164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
802165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
802166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
802167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
802168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
802169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
802170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
802268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
802270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
802362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
802368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
802374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
802375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
802376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
802377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
802390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
802493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
802494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
802495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
802497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
802592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
802608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
802609     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)'' 
802612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
802613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
802614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
802615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
802616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
802630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
802632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
802633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
802633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
802634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
802747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
802748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
802750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
802751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
802752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
802871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
802877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
802878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
802879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
802879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
802880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
802880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
803062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
803063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
803064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
803066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
803066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
803067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
803067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
803068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
803069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
803070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
803071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
803072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
803072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
803073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
803074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
803181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
803183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
803190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
803287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
803390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
803392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
803393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
803394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
803395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
803395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
803396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
803396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
803397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
803507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
803514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
803628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
803629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
803630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
803631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
803632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
803632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
803633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
803634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
803641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
803642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
803745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
803752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
803759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
803886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
803888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
803889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
803890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
803890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
803891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
803891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
803893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
803962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
803964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
803964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
803965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
803966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
803974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
803980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
804134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
804249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
804250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
804251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
804252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
804471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
804587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
804587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
808531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
808537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
808538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
808539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
808540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
808687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
808688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
808690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
808691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
808700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
808839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
812875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
817124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
817130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
817132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
817132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
817133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
817274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
817276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
817277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
817278     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)' ...' 
817280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
818792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
818792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
818793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
821789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
822772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
822774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
822774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
822782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
822794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
822797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
822799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
822800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
822804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
822806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
822809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
822812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
822813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
822822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
822824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
822824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
822883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
822884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
822884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
822885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
822885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
822969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
822970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
822972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
822973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
822973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
822978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
822979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
822980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
822981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
822982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
822983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
823097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
823099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
823099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
823101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
823102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
823103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
823223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
823224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
823225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
823226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
823227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
823228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
823229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
823229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
823230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
823231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
823232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
823232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
823233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
823234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
823235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
823235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
823236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
823237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
823239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
823242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
823289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
823291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
823361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
823362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
823364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
823366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
823367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
823367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
823426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
823430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
823431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
823433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
823435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
823436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
823436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
823489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
823493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
823496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
823562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
823632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
823632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.8ns 
823633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
826708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
827728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
827775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.57ms