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

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

tests
0

failures
0

ignored
10m10.31s

duration
100%

successful

Tests

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

Standard output

539        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
561        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8ms 
754        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766        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)

1655       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1658       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1662       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1662       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2993       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8073       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.32s 
8164       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8197       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ns 
8213       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8213       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
8218       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
10960      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11837      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.44ms 
11846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.1ns 
11848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
14368      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15227      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
15230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.6ns 
15232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
17648      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18433      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
18437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.02ms 
18439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
20773      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21546      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
21548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.3ns 
21549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
23874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24667      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.13ms 
24670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.28ms 
24673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
26991      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.56ms 
27763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357ns 
27764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30076      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
30076      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30828      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703ns 
30832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30832      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.8ns 
30833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
33139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33870      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.4ns 
33872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.6ns 
33874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
36150      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
36897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
36899      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.4ns 
36900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
36900      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
36901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
39165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.9ns 
39914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.5ns 
39916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
42236      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 506.6ns 
42989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.5ns 
42991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
45238      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46068      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.62ms 
46076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46076      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345ns 
46078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
48337      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49211      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.9ms 
49216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.3ns 
49219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
51489      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
52449      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 204.31ms 
52452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
52452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.5ns 
52453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
54699      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
55441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
55447      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
55449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
55450      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.8ns 
55451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
57702      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
58442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
58445      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
58449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
58449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318ns 
58450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60681      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
60682      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
61434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
61483      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.3ms 
61487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
61487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.7ns 
61488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63743      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
63743      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
64454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
64468      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.56ms 
64469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
64470      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
64470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66715      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
66715      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
67445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
67458      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
67460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
67460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
67461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
69701      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
70431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
70446      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 
70448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
70449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 
70450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72687      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
72688      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
73417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
73431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.31ms 
73433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
73433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.6ns 
73434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
75679      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
76408      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
76431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.05ms 
76433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
76433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns 
76434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
78680      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
79389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
79392      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
79393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
79393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
79394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
81637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
82375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
82420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.77ms 
82422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
82422      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
82423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
84652      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
85390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
85443      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.7ms 
85446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
85447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.4ns 
85448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
87693      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
88428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
88480      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.73ms 
88484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
88485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 779.6ns 
88486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
90712      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
91442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
91450      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
91453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
91453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 605.2ns 
91455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
93698      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
94411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
94423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
94424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
94425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
94425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
96677      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
97403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
97414      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
97415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
97415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
97416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
99635      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
100362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
100370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
100371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
100372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
100372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
102617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
103347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
103358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
103363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
103364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.2ns 
103365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
105588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
106315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
106325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
106328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
106328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.6ns 
106329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
108572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
109280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
109284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
109286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
109286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.8ns 
109287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
111541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
112268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
112277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
112278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
112278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
112279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
114503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
115228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
115273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.14ms 
115274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
115274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
115275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
117524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
118249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
118264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
118266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
118267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 
118268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
120489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
121214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
121229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
121236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
121236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
121237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
123464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
124172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
124188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
124189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
124189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
124190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
126415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
127139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
127154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
127156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
127156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
127157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
129363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
130089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
130125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.29ms 
130128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
130128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
130129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
132368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
133094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
133096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
133097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
133097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
133098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
135322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
136046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
136050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
136052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
136052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
136052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
138279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
138984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
138991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
138992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
138992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
138993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
141216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
141943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
141953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.32ms 
141954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
141954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
141955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
144164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
144887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
144904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
144905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
144905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
144906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
147134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
147858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
147869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
147872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
147872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
147873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
150100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
150834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
150836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
150838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
150838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.2ns 
150839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
153076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
153784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
153788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
153789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
153789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
153790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
156045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
156771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
156775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
156776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
156777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
156777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
158992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
159717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
159781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.26ms 
159783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
159783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 
159784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
162014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
162739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
162813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.35ms 
162815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
162816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 
162817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
165027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
165751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
165754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
165756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
165756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
165756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
167994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
168699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
168731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.7ms 
168733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
168733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
168734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
170968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
171708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
171736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
171738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
171738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.5ns 
171739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
173952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
174676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
174678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
174680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
174680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
174681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
176905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
177631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
177774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.65ms 
177776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
177776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 
177777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
180002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
180729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
180739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
180740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
180740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
180741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
182987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
183691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
183698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
183700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
183700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
183700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
185924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
186647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
186662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
186663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
186663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
186663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
188877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
189603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
189613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
189615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
189615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
189615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
191835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
192553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
192556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
192557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
192557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
192558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
194759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
195482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
195486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
195487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
195487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
195487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
197710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
198416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
198436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.56ms 
198437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
198437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
198438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
200666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
201390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
201405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.81ms 
201406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
201406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
201407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
203621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
204348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
204361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.45ms 
204363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
204363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
204363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
206585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
207306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
207310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
207311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
207311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
207312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
209527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
210252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
210256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
210257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
210257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
210258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
212482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
213185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
213190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
213191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
213191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
213192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
215411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
216135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
216137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
216139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
216139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
216139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
218342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
219065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
219067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.3ns 
219068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
219068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
219069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
221295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
222016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
222020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
222021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
222021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
222022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
224235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
224956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
224958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.7ns 
224959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
224959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
224960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
227180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
227883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
227945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.11ms 
227948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
227948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.6ns 
227949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
230242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
230971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
231008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.06ms 
231010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
231010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173ns 
231011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
233224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
233948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
233979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.62ms 
233981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
233981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
233981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
236221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
236944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
236991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.89ms 
236992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
236992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
236993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
239202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
239926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
239955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.69ms 
239956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
239956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
239957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
242185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
242888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
242936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.87ms 
242937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
242937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
242938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
245195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
245919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
245945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.13ms 
245946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
245946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
245947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
248156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
248880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
248898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms 
248899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
248899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
248900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
251134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
251858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
251881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.65ms 
251882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
251883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 812.8ns 
251884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
254091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
254821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
254840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms 
254841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
254841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
254842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
257084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
257786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
257812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.11ms 
257813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
257814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
257814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
260040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
260772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
260796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.62ms 
260797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
260797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
260798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
263004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
263726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
263755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.25ms 
263757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
263758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.9ns 
263760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
265988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
266708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
266731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.27ms 
266733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
266733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
266733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
268941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
269667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
269686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.74ms 
269687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
269687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
269688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
271924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
272626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
272650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.03ms 
272651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
272651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
272652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
274886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
275610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
275633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.92ms 
275635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
275635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
275635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
277840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
278571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
278578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
278579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
278579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
278579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
280795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
281518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
281534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms 
281535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
281535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
281536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
283747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
284474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
284477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
284479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
284479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
284479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
286702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
287405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
287407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.5ns 
287408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
287408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
287409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
289626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
290352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
290354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743ns 
290356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
290356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
290357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
292570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
293299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
293305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
293307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
293307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
293307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
295531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
296254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
296260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
296261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
296261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
296262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
298470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
299196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
299208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms 
299210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
299210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175ns 
299211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
301440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
302144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
302147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
302148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
302148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
302149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
304368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
305092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
305094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.3ns 
305095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
305095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
305096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
307303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
308034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
308039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
308040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
308040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
308041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
310261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
310983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
310985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.2ns 
310986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
310986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
310987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
313191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
313914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
313916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 529.1ns 
313917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
313917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
313918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
316145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
316848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
316850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.3ns 
316851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
316851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
316852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
319091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
319834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
319838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
319839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
319839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
319839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
322042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
322768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
322781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
322783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
322783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.4ns 
322784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
325003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
325724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
325728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
325729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
325729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
325729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
327929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
328656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
328663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
328664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
328664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
328665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
330888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
331593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
331598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
331603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
331603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
331604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
333830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
334554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
334568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.96ms 
334570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
334570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
334570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
336792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
337495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
337498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
337499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
337499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
337500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
339717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
340440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
340443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
340444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
340444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
340445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
342665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
343368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
343372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
343373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
343373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
343374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
345585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
346305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
346321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.37ms 
346322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
346322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
346323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
348548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
349253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
349256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.1ns 
349259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
349259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
349260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
351473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
352194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
352230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.83ms 
352231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
352231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
352232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
354434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
355159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
355162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
355164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
355164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
355164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
357380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
358101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
358121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.29ms 
358123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
358123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.3ns 
358124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
360354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
361057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
361077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms 
361078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
361078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
361079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
363300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
364023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
364046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ms 
364047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
364047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
364048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
366273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
367001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
367003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.3ns 
367004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
367004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
367004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
369209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
369929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
369935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
369936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
369936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
369936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
372154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
372879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
372881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
372882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
372882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
372883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
375081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
375806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
375809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.4ns 
375811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
375811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
375812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
378029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
378754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
378757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.5ns 
378758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
378758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
378759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
380979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
381704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
381707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
381708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
381708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
381709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
383914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
384640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
384643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
384644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
384644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
384645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
386860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
387586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
387595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
387596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
387596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
387601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
389836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
390568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
390580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
390581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
390581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
390582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
392784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
393514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
393527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
393529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
393529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.3ns 
393530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
395747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
396476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
396490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms 
396491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
396491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
396492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
398707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
399439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
399443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
399444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
399444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
399445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
401644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
402374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
402380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
402381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
402381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
402382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
404598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
405327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
405329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.4ns 
405330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
405330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
405331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
407550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
408281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
408284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
408285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
408285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
408286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
410501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
411214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
411216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
411217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
411217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
411218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
413434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
414163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
414173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
414175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
414175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
414175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
416426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
417155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
417159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
417160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
417160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
417161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
419382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
420113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
420119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
420120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
420121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.4ns 
420121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
422371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
423101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
423103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.1ns 
423104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
423104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
423105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
425305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
426035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
426037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.4ns 
426039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
426039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.3ns 
426040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
428254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
428988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
428994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
428996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
428996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 
428997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
431211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
431944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
431946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
431947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
431948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
431948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
434164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
434900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
434903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
434904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
434904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
434904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
437116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
437846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
437849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
437850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
437850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
437851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
440068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
440799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
440804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
440805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
440805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
440806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
443028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
443739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
443742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
443743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
443743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
443743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
445955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
446685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
446695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
446696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
446696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
446697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
448914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
449645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
449647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.9ns 
449648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
449648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
449648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
451865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
452596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
452602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
452603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
452603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
452604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
454840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
455584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
455588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.3ns 
455591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
455591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.3ns 
455592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
457827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
458556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
458558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.4ns 
458559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
458560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
458560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
460773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
461509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
461514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
461515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
461515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
461516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
463730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
464461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
464463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
464465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
464465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
464465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
466675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
467407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
467410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
467411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
467411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
467412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
469625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
470358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
470362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
470363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
470363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
470364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
472576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
473309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
473313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
473314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
473314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
473315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
475529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
476263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
476279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.97ms 
476280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
476280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
476281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
478570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
479333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
479348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
479349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
479349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
479350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
481650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
482412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
482422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ms 
482423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
482423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
482424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
484728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
485491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
485502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
485503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
485503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
485504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
487782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
488519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
488543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
488544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
488544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
488545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
490795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
491533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
491558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.24ms 
491559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
491559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
491559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
493789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
494526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
494549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms 
494551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
494551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
494551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
496764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
497501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
497515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
497516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
497516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
497517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
499729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
500465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
500494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.51ms 
500495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
500495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
500496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
502713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
503454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
503499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.77ms 
503500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
503500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
503501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
505715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
506451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
506488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.42ms 
506489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
506489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
506490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
508725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
509464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
509506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.7ms 
509508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
509508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
509509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
511726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
512461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
512504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.82ms 
512505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
512506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
512506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
514725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
515464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
515581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.49ms 
515585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
515585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns 
515586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
517808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
518545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
518553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
518554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
518554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
518555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
520780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
521517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
521524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
521525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
521525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
521526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
523734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
524470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
524474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
524475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
524476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
524476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
526687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
527424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
527441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
527442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
527442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
527443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
529673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
530409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
530419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
530420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
530420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
530421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
532639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
533381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
533384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
533385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
533385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
533386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
535598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
536333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
536350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.01ms 
536351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
536351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
536351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
538614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
539349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
539365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
539366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
539366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
539366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
541583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
542319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
542337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
542338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
542338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
542339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
544561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
545298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
545301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
545302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
545302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
545302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
547530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
548265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
548268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
548269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
548269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
548270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
550483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
551220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
551226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
551227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
551227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
551227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
553458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
554192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
554198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
554199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
554199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
554199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
556408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
557144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
557212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.29ms 
557214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
557214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
557214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
559456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
560196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
560224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.84ms 
560226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
560226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
560227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
562447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
563181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
563202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.77ms 
563203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
563203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
563204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
565432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
566167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
566169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.9ns 
566171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
566171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 
566172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
568382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
569121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
569319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.11ms 
569321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
569321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.5ns 
569322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
571578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
572318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
572367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.68ms 
572369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
572369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.7ns 
572370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
574583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
575337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
575338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.3ns 
575339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
575339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
575340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
577554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
578289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
578291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.4ns 
578292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
578292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
578293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
580521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
581257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
581259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.8ns 
581260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
581260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
581261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
583473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
584209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
584211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.5ns 
584212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
584212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
584213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
586441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
587177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
587266     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
587283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.92ms 
587285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
587285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
587286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
589547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
590286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
590329     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
590329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.37ms 
590330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
590330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
590332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
592559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
593302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
593303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
593328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
593377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
593398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
593405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
593417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
593419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
593421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
593424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
593427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
593428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
593434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
593435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
593607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
593608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
593609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
593610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
593611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
593709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
593710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
593711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
593713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
593714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
593715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
593860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
593861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
593862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
593863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
593864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
593865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
593991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
593992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
593993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
593994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
593995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
593996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
594001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
594002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
594003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
594004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
594005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
594006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
594012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
594012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
594013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
594014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
594015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
594016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
594122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
594124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
594125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
594225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
594226     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)'' 
594229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
594230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
594230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
594231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
594232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
594233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
594236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
594237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
594238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
594239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
594240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
594328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
594331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
594332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
594333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
594334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
594335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
594337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
594435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
594439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
594440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
594442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
594443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
594443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
594444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
594446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
594523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
594524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
594599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
594602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
594606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
594608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
594610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
594611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
594612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
594613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
594614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
594615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
594622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
594625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
594703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
594705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
594706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
594707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
594708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
594708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
594709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
594710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
594755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
594759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
594837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
594838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
594840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
594842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
594843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
594843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
594973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
594976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
594979     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)'' 
594981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
594983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
594984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
594984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
594985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
594994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
594995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
594996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
594997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
595087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
595089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
595090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
595090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
595092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
595093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
595183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
595184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
595185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
595187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
595187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
595188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
595189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
595190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
595262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
595263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
595331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
595332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
595332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
595336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
595339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
595343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
595450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
595453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
595454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
595454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
595463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
595538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
599713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
599714     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)'' 
599719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
599720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
599720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
599721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
599721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
599728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
599729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
599730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
599731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
599731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
599818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
599821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
599822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
599823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
599823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
599824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
599824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
599913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
599914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
599915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
599916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
599916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
599917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
599917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
599918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
600028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
600029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
600161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
600165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
600169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
600170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
600170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
600172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
600182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
600261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
600262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
600262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
600263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
600331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
600339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
600340     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)'' 
600342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
600343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
600343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
600344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
600344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
600354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
600355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
600356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
600356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
600357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
600439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
600440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
600441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
600442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
600442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
600533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
600537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
600538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
600539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
600539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
600540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
600541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
600632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
600634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
600634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
600636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
600636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
600637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
600637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
600639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
600640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
600641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
600642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
600643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
600643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
600644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
600645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
600725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
600726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
600731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
600803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
600877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
600878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
600879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
600879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
600880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
600880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
600881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
600881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
600882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
600961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
600966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
601048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
601049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
601050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
601051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
601051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
601051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
601052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
601052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
601057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
601057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
601131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
601135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
601140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
601232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
601233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
601233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
601234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
601235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
601235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
601235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
601236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
601286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
601287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
601288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
601288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
601289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
601294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
601299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
601407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
601489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
601490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
601490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
601491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
601662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
601746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
601747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
604559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
604565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
604566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
604566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
604567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
604676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
604677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
604678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
604679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
604680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
604816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
607553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
610517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
610522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
610522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
610523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
610524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
610630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
610631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
610632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
610633     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)' ...' 
610634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
611708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
611708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
611709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
614060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
614816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
614817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
614817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
614825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
614836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
614838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
614840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
614840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
614845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
614846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
614849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
614852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
614852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
614861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
614862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
614863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
614904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
614905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
614905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
614905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
614906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
614960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
614960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
614962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
614962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
614963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
614966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
614966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
614966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
614967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
614968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
614968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
615034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
615034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
615035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
615036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
615037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
615037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
615098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
615098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
615099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
615099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
615100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
615100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
615101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
615101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
615102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
615102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
615103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
615103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
615104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
615104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
615104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
615105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
615105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
615106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
615107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
615109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
615136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
615138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
615179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
615180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
615182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
615183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
615184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
615184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
615221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
615223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
615224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
615225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
615226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
615227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
615228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
615266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
615268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
615270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
615317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
615364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
615364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
615365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
617749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
618524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
618555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.16ms