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

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

tests
0

failures
0

ignored
13m43.03s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.927s passed
powPositiveConcrete data()[101] 3.997s passed
powGeq1Concrete data()[102] 3.925s passed
pow2InIntLower data()[103] 3.940s passed
pow2InIntUpper data()[104] 3.935s passed
logSelfConcrete data()[105] 3.932s passed
log1Concrete data()[106] 3.972s passed
logProduct data()[107] 3.973s passed
logTimesBaseConcrete data()[108] 3.936s passed
logProdIdentity data()[109] 3.950s passed
moduloByteIsInByte data()[10] 4.129s passed
logProdIdentityConcrete data()[110] 3.907s passed
logPowIdentity data()[111] 3.933s passed
logPowIdentityConcrete data()[112] 3.904s passed
logPositive data()[113] 3.932s passed
logPositiveConcrete data()[114] 3.976s passed
logMono data()[115] 3.975s passed
logMonoConcrete data()[116] 3.967s passed
powLogLess data()[117] 4.000s passed
powLogMore2 data()[118] 4.017s passed
logLessThanPow data()[119] 4.056s passed
moduloCharIsInChar data()[11] 4.039s passed
logLessThanPowConcrete data()[120] 3.982s passed
logSqueeze data()[121] 3.965s passed
ifthenelse_equals data()[122] 3.968s passed
ifthenelse_equals_1 data()[123] 3.975s passed
ifthenelse_equals_2 data()[124] 3.951s passed
disjointWithSingleton1 data()[125] 3.931s passed
disjointWithSingleton2 data()[126] 3.987s passed
disjointArrayRanges data()[127] 4.033s passed
disjointArrayRangeAllFields1 data()[128] 4.005s passed
disjointArrayRangeAllFields2 data()[129] 3.981s passed
div_unique1 data()[12] 4.162s passed
seqSelfDefinition data()[130] 4.024s passed
seqOutsideValue data()[131] 3.987s passed
castedGetAny data()[132] 4.020s passed
seqGetAlphaCast data()[133] 3.961s passed
getOfSeqSingleton data()[134] 4.047s passed
getOfSeqSingletonConcrete data()[135] 3.943s passed
getOfSeqConcat data()[136] 4.036s passed
getOfSeqSub data()[137] 4.011s passed
getOfSeqReverse data()[138] 4.027s passed
lenOfSeqEmpty data()[139] 4.039s passed
div_unique2 data()[13] 4.220s passed
lenOfSeqSingleton data()[140] 3.998s passed
lenOfSeqConcat data()[141] 4.005s passed
lenOfSeqSub data()[142] 3.975s passed
lenOfSeqReverse data()[143] 3.978s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.964s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.021s passed
getOfSeqSingletonEQ data()[146] 4.023s passed
getOfSeqConcatEQ data()[147] 4.010s passed
getOfSeqSubEQ data()[148] 3.994s passed
getOfSeqReverseEQ data()[149] 4.005s passed
div_exists data()[14] 4.416s passed
lenOfSeqEmptyEQ data()[150] 3.987s passed
lenOfSeqSingletonEQ data()[151] 3.944s passed
lenOfSeqConcatEQ data()[152] 4.025s passed
lenOfSeqSubEQ data()[153] 3.997s passed
lenOfSeqReverseEQ data()[154] 3.996s passed
getOfSeqDefEQ data()[155] 3.959s passed
lenOfSeqDefEQ data()[156] 3.961s passed
seqConcatWithSeqEmpty1 data()[157] 3.969s passed
seqConcatWithSeqEmpty2 data()[158] 3.992s passed
seqReverseOfSeqEmpty data()[159] 4.046s passed
div_one data()[15] 4.119s passed
subSeqComplete data()[160] 3.966s passed
subSeqTailR data()[161] 4.057s passed
subSeqTailL data()[162] 4.004s passed
subSeqTailEQR data()[163] 4.034s passed
subSeqTailEQL data()[164] 4.035s passed
seqDef_split data()[165] 4.017s passed
seqDef_induction_upper data()[166] 4.126s passed
seqDef_induction_upper_concrete data()[167] 4.079s passed
seqDef_induction_lower data()[168] 4.051s passed
seqDef_induction_lower_concrete data()[169] 4.044s passed
jdiv_one data()[16] 4.099s passed
seqDef_split_in_three data()[170] 4.214s passed
seqDef_empty data()[171] 4.062s passed
seqDef_one_summand data()[172] 3.997s passed
seqDef_lower_equals_upper data()[173] 3.973s passed
seqDefOfSeq data()[174] 4.004s passed
seqSelfDefinitionEQ2 data()[175] 3.952s passed
indexOfSeqSingleton data()[176] 3.974s passed
indexOfSeqConcatFirst data()[177] 4.010s passed
indexOfSeqConcatSecond data()[178] 4.000s passed
indexOfSeqSub data()[179] 4.058s passed
div_zero data()[17] 4.145s passed
lenOfArray2seq data()[180] 4.017s passed
getAnyOfArray2seq data()[181] 3.999s passed
getOfArray2seq data()[182] 4.002s passed
getAnyOfNPermInv data()[183] 3.996s passed
seqNPermRange data()[184] 4.082s passed
seqPermTrans data()[185] 4.019s passed
seqPermRefl data()[186] 3.995s passed
seqPermSplit data()[187] 3.973s passed
seqNPermRight data()[188] 4.268s passed
seqPermFromSwap data()[189] 4.073s passed
divResZero1 data()[18] 4.062s passed
seqPermTransAlt0 data()[190] 3.969s passed
seqPermTransAlt1 data()[191] 4.037s passed
seqPermTransAlt2 data()[192] 3.941s passed
seqPermTransAlt3 data()[193] 4.021s passed
seqPermForall data()[194] 4.130s passed
seqPermExists data()[195] 4.099s passed
schiffl_lemma_2 data()[196] 27.864s passed
schiffl_thm_1 data()[197] 4.935s passed
eqSameSeq data()[198] 4.095s passed
divResZero2 data()[19] 4.109s passed
eqTermCut data()[1] 4.870s passed
divResOne1 data()[20] 4.027s passed
divResOne2 data()[21] 4.012s passed
div_cancel1 data()[22] 4.073s passed
div_cancel2 data()[23] 3.994s passed
divAddMultDenom data()[24] 4.043s passed
divMinus data()[25] 4.131s passed
divMinusDenom data()[26] 4.175s passed
divLeastDPos data()[27] 4.010s passed
divLeastDNeg data()[28] 3.979s passed
divGreatestDPos data()[29] 3.991s passed
equivAllRight data()[2] 4.616s passed
divGreatestDNeg data()[30] 4.007s passed
divIncreasingPos data()[31] 4.037s passed
divIncreasingNeg data()[32] 4.031s passed
jdiv_zero data()[33] 4.050s passed
jdivPulloutMinusNum data()[34] 4.017s passed
jdivPulloutMinusDenom data()[35] 4.148s passed
jdiv_uniquePosPos data()[36] 4.031s passed
jdiv_uniquePosNeg data()[37] 4.036s passed
jdiv_uniqueNegPos data()[38] 4.047s passed
jdiv_uniqueNegNeg data()[39] 4.027s passed
irrflConcrete1 data()[3] 4.437s passed
jdivMultDenom1 data()[40] 4.046s passed
jdivMultDenom2 data()[41] 4.044s passed
mod_geZero data()[42] 4.051s passed
mod_lessDenom data()[43] 4.043s passed
jmod_NumPos data()[44] 4.029s passed
jmod_NumNeg data()[45] 4.131s passed
jmod_geZero data()[46] 3.980s passed
jmodNumZero data()[47] 4.006s passed
jmod_pulloutminusNum data()[48] 3.994s passed
jmod_pulloutminusDenom data()[49] 3.977s passed
irrflConcrete2 data()[4] 4.206s passed
jmodUnique1 data()[50] 4.107s passed
jmodUnique2 data()[51] 4.101s passed
intDivRem data()[52] 4.011s passed
jmodjmod data()[53] 3.993s passed
jmodDivisible data()[54] 4.007s passed
jmodDivisibleRep data()[55] 3.984s passed
jdivAddMultDenom data()[56] 4.237s passed
jmodAltZero data()[57] 3.911s passed
jmodAddMultDenomZero data()[58] 4.032s passed
polyDiv_zero data()[59] 4.024s passed
cancel_gtPos data()[5] 4.212s passed
polyMod_ltdivDenom data()[60] 3.941s passed
bsum_empty data()[61] 3.989s passed
bsum_induction_upper data()[62] 4.005s passed
bsum_induction_lower data()[63] 3.994s passed
bsum_num_of_bounds data()[64] 4.028s passed
bsum_num_of_bounds2 data()[65] 4.012s passed
bsum_induction_upper2 data()[66] 3.938s passed
bsum_induction_upper_concrete data()[67] 3.959s passed
bsum_induction_upper_concrete_2 data()[68] 3.979s passed
bsum_induction_upper2_concrete data()[69] 3.920s passed
cancel_gtNeg data()[6] 4.199s passed
bsum_induction_lower_concrete data()[70] 3.950s passed
bsum_induction_lower2 data()[71] 3.949s passed
bsum_induction_lower2_concrete data()[72] 3.958s passed
bsum_positive data()[73] 4.043s passed
bsum_upper_bound data()[74] 4.033s passed
bsum_lower_bound data()[75] 4.135s passed
bsum_positive_lower_bound_element data()[76] 4.056s passed
bsum_sub_same_index data()[77] 4.042s passed
bsum_less_same_index data()[78] 4.081s passed
bsum_equal_except_one_index data()[79] 4.023s passed
moduloIntIsInInt data()[7] 4.158s passed
bsum_num_of_is_max data()[80] 3.985s passed
bsum_num_of_is_max2 data()[81] 4.068s passed
bsum_num_of_is_max3 data()[82] 3.986s passed
bsum_num_of_is_max4 data()[83] 3.958s passed
bsum_num_of_lt_max data()[84] 3.945s passed
bsum_num_of_lt_max2 data()[85] 4.011s passed
bsum_num_of_lt_max3 data()[86] 4.081s passed
bsum_num_of_lt_max4 data()[87] 3.984s passed
bsum_num_of_gt0 data()[88] 4.039s passed
bsum_num_of_gt0_alt data()[89] 4.028s passed
moduloLongIsInLong data()[8] 4.126s passed
bsum_add_concrete data()[90] 3.967s passed
bprod_all_positive data()[91] 4.016s passed
bprod_split data()[92] 3.968s passed
powConcrete0 data()[93] 3.996s passed
powConcrete1 data()[94] 3.967s passed
powSplitFactor data()[95] 3.993s passed
powAdd data()[96] 3.963s passed
powMono data()[97] 3.992s passed
powMonoConcrete data()[98] 3.967s passed
powMonoConcreteRight data()[99] 3.969s passed
moduloShortIsInShort data()[9] 4.167s passed

Standard output

993        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
1022       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.24ms 
1318       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1337       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)

2371       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2373       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2375       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2375       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4424       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.55s 
10949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.2ns 
11018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11020      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.78ms 
11028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
14674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.82ms 
15890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.2ns 
15893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19428      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
19428      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20502      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.84ms 
20507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.6ns 
20512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
23866      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24942      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
24945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 728.92ns 
24947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
28127      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29148      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
29154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.61ns 
29156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
32293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.52ms 
33366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33367      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1ms 
33370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
36501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37562      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.11ms 
37565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.21ns 
37566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40716      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
40716      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
41717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
41721      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.22ns 
41724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
41724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.91ns 
41725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
44841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
45844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
45847      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.51ns 
45850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
45851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.41ns 
45852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
48980      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50015      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.21ns 
50017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 
50018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
53133      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54144      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.91ns 
54146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211ns 
54148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
57141      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58183      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
58188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 590.11ns 
58190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
61267      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
62343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.17ms 
62352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
62352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.01ns 
62353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
65528      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
66563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.91ms 
66573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
66573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.01ns 
66577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
69634      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
70645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
70985      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 328.11ms 
70990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
70990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.4ns 
70991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
74095      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75106      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
75108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.71ns 
75110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78173      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
78175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
79209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 800.82ns 
79212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
82281      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
83293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
83351      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.94ms 
83355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
83356      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.41ns 
83357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
86428      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
87391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
87414      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.85ms 
87417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
87417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.61ns 
87419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90511      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
90512      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
91501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
91523      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.49ms 
91527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
91528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.41ns 
91533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
94530      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
95525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
95550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.95ms 
95553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
95554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.91ns 
95555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98567      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
98568      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
99538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
99563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.85ms 
99566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
99567      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.15ms 
99568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
102609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
103600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
103636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.18ms 
103638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
103639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.81ns 
103640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
106644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
107626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
107630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
107633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
107633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.11ns 
107635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
110638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
111610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
111674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.57ms 
111676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
111676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
111677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
114718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
115675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
115803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.27ms 
115808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
115808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 
115809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
118909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
119909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
119979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.04ms 
119982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
119982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.11ns 
119984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
123014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
123980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
123991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
123992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
123992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
123993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
127008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
127950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
127969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms 
127970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
127970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
127971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
130944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
131943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
131960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
131961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
131961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
131963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
134988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
135956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
135967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
135968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
135968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
135969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
139036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
139993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
140004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
140006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
140006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
140007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
143032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
144020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
144034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
144037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
144037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.51ns 
144040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
147084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
148080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
148085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
148086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
148087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
148087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
151095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
152086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
152102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
152104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
152104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
152105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
155145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
156148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
156243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.23ms 
156253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
156254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.41ns 
156255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
159259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
160249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
160283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.76ms 
160285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
160285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
160287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
163320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
164291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
164319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.85ms 
164321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
164321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.5ns 
164322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
167356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
168338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
168365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.94ms 
168368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
168368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.91ns 
168369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
171396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
172368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
172394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.19ms 
172395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
172395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
172396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
175401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
176374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
176439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.11ms 
176449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
176449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.91ns 
176451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
179532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
180487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
180490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
180492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
180492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
180493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
183542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
184533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
184540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
184543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
184543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
184544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
187579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
188573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
188584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
188585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
188586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
188586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
191604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
192601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
192613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
192615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
192615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
192616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
195698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
196697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
196744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.57ms 
196746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
196746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.41ns 
196747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
199742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
200712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
200724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
200726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
200726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
200727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
203721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
204722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
204726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
204734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
204735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.91ns 
204736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
207791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
208719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
208725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
208726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
208726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
208727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
211724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
212696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
212701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
212703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
212703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
212704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
215693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
216688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
216807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.44ms 
216812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
216813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.61ns 
216814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
219807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
220775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
220910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.88ms 
220913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
220913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.21ns 
220914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
223943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
224917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
224922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
224925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
224925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.31ns 
224926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
227896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
228861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
228914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.03ms 
228918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
228918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.41ns 
228919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
231930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
232877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
232922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.13ms 
232924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
232925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.2ns 
232926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
235918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
236900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
236905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
236913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
236913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.11ns 
236915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
239926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
240904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
241146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.38ms 
241148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
241148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
241149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
244121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
245043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
245059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.19ms 
245060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
245060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
245061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
248128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
249079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
249090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
249092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
249092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
249093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
252113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
253086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
253113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.02ms 
253116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
253116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.81ns 
253117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
256062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
257034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
257053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
257057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
257058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 
257059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
260082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
261039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
261044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
261046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
261046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
261047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
264057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
265043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
265049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
265051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
265051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
265052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
268042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
269005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
269039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.26ms 
269046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
269047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.61ns 
269048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
272085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
273047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
273072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.65ms 
273074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
273074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
273075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
276063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
277061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
277084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
277086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
277086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 
277087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
280043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
281017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
281022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
281024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
281024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248ns 
281025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
284003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
284976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
284981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
284983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
284983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
284984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
287984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
288953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
288960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
288961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
288962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
288962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
291919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
292876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
292880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
292881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
292881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
292882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
295854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
296828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
296831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.52ns 
296832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
296832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
296833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
299826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
300774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
300779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
300781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
300781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
300782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
303773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
304733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
304738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
304740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
304740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 
304741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
307743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
308711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
308780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.73ms 
308783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
308783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.1ns 
308784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
311796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
312726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
312803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.38ms 
312815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
312816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.01ns 
312817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
315892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
316891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
316948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.91ms 
316950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
316950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
316951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
319976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
320933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
321005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.77ms 
321006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
321006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
321007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
324053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
324994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
325047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.96ms 
325048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
325048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
325049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
328078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
329045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
329126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.12ms 
329129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
329129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.61ns 
329131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
332144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
333109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
333150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.55ms 
333152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
333152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.8ns 
333153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
336125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
337103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
337135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.9ms 
337136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
337137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
337138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
340210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
341167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
341203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.09ms 
341205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
341205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
341206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
344179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
345160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
345189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.22ms 
345191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
345191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
345192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
348144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
349104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
349147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.88ms 
349149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
349149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
349150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
352121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
353050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
353092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.03ms 
353094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
353094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
353095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
356074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
357062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
357101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.83ms 
357105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
357105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.71ns 
357107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
360176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
361149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
361184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.22ms 
361185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
361186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
361186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
364189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
365139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
365168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.32ms 
365170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
365170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
365171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
368213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
369174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
369207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.98ms 
369209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
369209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
369210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
372220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
373199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
373235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.1ms 
373237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
373237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 587.52ns 
373238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
376246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
377193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
377202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
377204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
377204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.11ns 
377205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
380222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
381193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
381218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.14ms 
381220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
381220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
381221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
384198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
385181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
385186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
385188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
385188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
385189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
388207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
389180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
389182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.82ns 
389184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
389184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
389185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
392164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
393146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
393149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
393151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
393151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.81ns 
393152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
396154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
397131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
397140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
397143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
397143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
397144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
400108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
401090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
401105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
401108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
401108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.01ns 
401109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
404143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
405080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
405098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.82ms 
405099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
405099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
405100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
408066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
409060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
409064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
409065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
409066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
409066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
412027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
413029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
413033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.02ns 
413034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
413035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
413035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
416007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
416951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
416960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
416962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
416962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.41ns 
416963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
419985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
420954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
420957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.22ns 
420958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
420958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
420959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
423916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
424879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
424882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.42ns 
424883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
424883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
424884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
427859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
428819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
428822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.42ns 
428824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
428824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
428825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
431776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
432750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
432757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
432759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
432760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.91ns 
432760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
435712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
436677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
436690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.02ms 
436691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
436691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
436692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
439692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
440656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
440661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
440663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
440663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
440663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
443663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
444625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
444634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
444636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
444636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
444637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
447587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
448565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
448570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
448572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
448572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
448573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
451526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
452500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
452521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
452522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
452522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
452523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
455490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
456423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
456427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
456429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
456429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
456429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
459396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
460356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
460360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
460362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
460362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
460362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
463291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
464260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
464264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
464265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
464266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
464266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
467221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
468170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
468196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
468199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
468199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.61ns 
468200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
471176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
472166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
472171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.92ns 
472175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
472176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.74ms 
472177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
475126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
476092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
476147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.04ms 
476149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
476149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
476150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
479138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
480110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
480115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
480116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
480116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
480117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
483107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
484082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
484114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.22ms 
484116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
484116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.81ns 
484117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
487124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
488104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
488131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.05ms 
488132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
488132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
488133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
491183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
492154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
492187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.45ms 
492189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
492189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
492190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
495185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
496166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
496169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.82ns 
496171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
496171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.61ns 
496172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
499176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
500127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
500135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
500136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
500136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
500137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
503128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
504099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
504102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
504104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
504104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
504104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
507125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
508074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
508077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.82ns 
508078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
508078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
508079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
511071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
512026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
512028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
512030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
512030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.31ns 
512031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
514968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
515955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
515959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
515962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
515962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
515962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
518957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
519941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
519946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
519952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
519952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.91ns 
519954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
522971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
523969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
523981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
523983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
523983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
523984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
526972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
527957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
527980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ms 
527989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
527989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.11ns 
527990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
530958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
531953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
531968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.68ms 
531970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
531970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.71ns 
531971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
534964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
535976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
535992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
535997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
535997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
535998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
538956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
539977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
539984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
539985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
539985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
539986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
542998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
543996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
544004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
544005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
544005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
544006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
546998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
547962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
547965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 943.13ns 
547966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
547966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
547967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
551014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
552008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
552011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
552012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
552012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
552013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
554994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
555950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
555954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
555956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
555957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.71ns 
555958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
558971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
559975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
559990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
559992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
559992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
559993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
562996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
563996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
564001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
564003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
564003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
564004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
567010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
568017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
568028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 
568030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
568030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.11ns 
568031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
571054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
572065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
572067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.93ns 
572069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
572069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
572069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
575064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
576063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
576066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.42ns 
576067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
576067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
576068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
579045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
580065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
580070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
580071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
580072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 
580072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
583043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
584042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
584046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
584047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
584047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
584048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
587023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
588015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
588023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
588025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
588025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
588026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
590997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
591984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
591988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
591989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
591989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
591990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
595004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
596001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
596008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
596009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
596010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
596010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
599016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
600025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
600032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
600033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
600033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
600034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
603040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
604026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
604041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
604042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
604043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
604043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
607049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
608032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
608035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
608037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
608037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
608037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
611029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
612030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
612040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 
612042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
612042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
612043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
615048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
616023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
616027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
616028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
616028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
616029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
618975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
619965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
619968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
619973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
619973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
619974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
622998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
623990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
623997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
623999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
623999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
624000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
627005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
627989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
627994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
627995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
627995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
627996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
630995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
631985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
631989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
631991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
631991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
631992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
634946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
635944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
635948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
635950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
635950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
635951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
638897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
639903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
639909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
639911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
639911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
639912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
642877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
643860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
643878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.11ms 
643879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
643880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
643880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
646877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
647850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
647871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.43ms 
647872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
647872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
647873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
650899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
651903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
651916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms 
651918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
651918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
651918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
654890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
655869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
655883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
655884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
655884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
655885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
658915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
659901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
659940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.78ms 
659941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
659941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
659942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
662922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
663907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
663943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.12ms 
663944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
663945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
663945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
666948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
667942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
667977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.45ms 
667979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
667979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
667980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
670987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
671993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
672012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.03ms 
672014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
672014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
672015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
674973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
675987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
676029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.88ms 
676031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
676031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
676032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
679091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
680089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
680155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.86ms 
680157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
680157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
680157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
683165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
684181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
684235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.67ms 
684236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
684236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
684237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
687228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
688227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
688285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.16ms 
688287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
688287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
688288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
691268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
692267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
692329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.38ms 
692331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
692331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
692332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
695354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
696377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
696543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 158.9ms 
696546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
696546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.71ns 
696547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
699580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
700595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
700606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
700607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
700607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
700608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
703588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
704591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
704602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
704603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
704604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
704604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
707574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
708568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
708575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
708576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
708576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
708577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
711551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
712555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
712579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.4ms 
712581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
712581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
712582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
715539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
716517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
716531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
716532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
716533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
716533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
719511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
720500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
720505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
720506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
720506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
720507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
723487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
724492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
724516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.38ms 
724517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
724517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
724518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
727504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
728493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
728516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.72ms 
728517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
728517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
728518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
731565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
732546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
732573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.88ms 
732574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
732574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
732575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
735583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
736584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
736590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
736591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
736591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
736592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
739590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
740584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
740589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
740591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
740591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
740592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
743582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
744583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
744591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
744592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
744593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
744593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
747578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
748579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
748587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
748588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
748588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
748589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
751586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
752571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
752669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.65ms 
752671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
752671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.7ns 
752672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
755644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
756649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
756688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.32ms 
756690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
756690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 
756691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
759654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
760651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
760683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.26ms 
760685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
760685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
760685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
763668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
764653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
764656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.61ns 
764658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
764658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
764659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
767661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
768656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
768924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 254.11ms 
768926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
768926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.71ns 
768927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
771938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
772926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
772997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.21ms 
772998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
772998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
772999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
775983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
776964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
776966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 415.01ns 
776968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
776968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
776969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
779985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
781001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
781003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 435.11ns 
781005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
781005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
781005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
783954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
784942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
784945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.91ns 
784946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
784946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
784947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
787978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
788963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
788965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.12ns 
788966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
788966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
788967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
791971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
792971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
793076     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
793095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.47ms 
793098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
793098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 483.31ns 
793100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
796117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
797128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
797194     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
797195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.91ms 
797197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
797197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
797198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
800217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
801236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
801237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
801274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
801316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
801335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
801339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
801346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
801348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
801349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
801351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
801354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
801356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
801358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
801359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
801640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
801642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
801643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
801646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
801647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
801811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
801813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
801814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
801816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
801818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
801819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
802069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
802072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
802073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
802074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
802075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
802076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
802246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
802248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
802249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
802250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
802252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
802253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
802262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
802263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
802264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
802266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
802268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
802269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
802278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
802279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
802280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
802281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
802282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
802284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
802468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
802469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
802471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
802667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
802669     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)'' 
802672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
802673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
802674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
802675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
802676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
802677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
802686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
802688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
802690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
802691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
802692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
802844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
802848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
802850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
802851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
802852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
802853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
802854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
803005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
803007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
803008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
803010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
803012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
803013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
803013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
803015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
803137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
803140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
803273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
803278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
803285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
803287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
803288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
803289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
803291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
803291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
803292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
803295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
803306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
803311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
803424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
803425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
803427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
803428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
803429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
803430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
803430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
803432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
803490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
803496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
803610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
803613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
803615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
803618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
803619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
803620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
803827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
803833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
803834     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)'' 
803836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
803837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
803838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
803839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
803840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
803850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
803852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
803853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
803854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
803977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
803979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
803980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
803981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
803982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
803983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
804124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
804126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
804127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
804129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
804129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
804130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
804131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
804132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
804242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
804244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
804349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
804350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
804351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
804357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
804362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
804367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
804529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
804531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
804532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
804533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
804547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
804658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
809189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
809191     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)'' 
809197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
809198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
809199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
809200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
809200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
809211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
809213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
809214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
809215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
809216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
809336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
809341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
809342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
809343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
809344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
809345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
809346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
809470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
809471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
809472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
809474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
809475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
809475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
809476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
809478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
809574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
809576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
809681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
809686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
809691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
809693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
809694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
809695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
809708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
809816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
809818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
809819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
809820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
809919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
809931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
809933     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)'' 
809935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
809936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
809937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
809938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
809938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
809952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
809954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
809955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
809956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
809957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
810070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
810072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
810074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
810074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
810075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
810192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
810197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
810198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
810199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
810199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
810200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
810201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
810329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
810330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
810331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
810333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
810333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
810334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
810334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
810336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
810337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
810337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
810339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
810339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
810340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
810340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
810341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
810453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
810454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
810462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
810563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
810663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
810665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
810666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
810667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
810668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
810669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
810669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
810669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
810671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
810784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
810791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
810981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
810982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
810983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
810984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
810985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
810985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
810987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
810988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
810994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
810995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
811102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
811109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
811116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
811246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
811247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
811248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
811249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
811249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
811250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
811250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
811251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
811318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
811321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
811322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
811323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
811325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
811334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
811341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
811487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
811597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
811598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
811599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
811600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
811808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
811915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
811916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
815653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
815660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
815662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
815663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
815663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
815805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
815806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
815808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
815809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
815810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
815946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
819647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
823514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
823519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
823520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
823521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
823522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
823659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
823660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
823662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
823663     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)' ...' 
823665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
825061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
825061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.4ns 
825062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
828255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
828255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
829221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
829223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
829223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
829234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
829247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
829250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
829252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
829253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
829258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
829260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
829264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
829266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
829267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
829278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
829280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
829281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
829343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
829344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
829345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
829345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
829346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
829426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
829427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
829428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
829429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
829430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
829434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
829435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
829436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
829437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
829438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
829439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
829530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
829531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
829531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
829534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
829535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
829536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
829627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
829628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
829629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
829629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
829630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
829631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
829632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
829632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
829634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
829634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
829635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
829635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
829636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
829637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
829637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
829638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
829639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
829640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
829641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
829644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
829680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
829682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
829736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
829738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
829739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
829741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
829742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
829742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
829793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
829796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
829797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
829800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
829801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
829802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
829802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
829854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
829858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
829862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
829926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
829996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
829996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
829997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
833010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
834045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
834089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.32ms