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

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

tests
0

failures
0

ignored
10m17.28s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 2.972s passed
powPositiveConcrete data()[101] 2.989s passed
powGeq1Concrete data()[102] 2.973s passed
pow2InIntLower data()[103] 2.983s passed
pow2InIntUpper data()[104] 2.997s passed
logSelfConcrete data()[105] 2.981s passed
log1Concrete data()[106] 2.994s passed
logProduct data()[107] 2.994s passed
logTimesBaseConcrete data()[108] 2.968s passed
logProdIdentity data()[109] 3.023s passed
moduloByteIsInByte data()[10] 3.026s passed
logProdIdentityConcrete data()[110] 2.985s passed
logPowIdentity data()[111] 2.985s passed
logPowIdentityConcrete data()[112] 2.973s passed
logPositive data()[113] 3.002s passed
logPositiveConcrete data()[114] 2.983s passed
logMono data()[115] 3.010s passed
logMonoConcrete data()[116] 2.976s passed
powLogLess data()[117] 3.009s passed
powLogMore2 data()[118] 3.009s passed
logLessThanPow data()[119] 3.016s passed
moduloCharIsInChar data()[11] 3.040s passed
logLessThanPowConcrete data()[120] 3.007s passed
logSqueeze data()[121] 2.993s passed
ifthenelse_equals data()[122] 2.990s passed
ifthenelse_equals_1 data()[123] 2.973s passed
ifthenelse_equals_2 data()[124] 2.984s passed
disjointWithSingleton1 data()[125] 2.985s passed
disjointWithSingleton2 data()[126] 2.985s passed
disjointArrayRanges data()[127] 3.002s passed
disjointArrayRangeAllFields1 data()[128] 2.997s passed
disjointArrayRangeAllFields2 data()[129] 2.989s passed
div_unique1 data()[12] 3.067s passed
seqSelfDefinition data()[130] 3.004s passed
seqOutsideValue data()[131] 2.997s passed
castedGetAny data()[132] 2.994s passed
seqGetAlphaCast data()[133] 2.987s passed
getOfSeqSingleton data()[134] 2.989s passed
getOfSeqSingletonConcrete data()[135] 2.996s passed
getOfSeqConcat data()[136] 2.994s passed
getOfSeqSub data()[137] 2.985s passed
getOfSeqReverse data()[138] 3.009s passed
lenOfSeqEmpty data()[139] 2.995s passed
div_unique2 data()[13] 3.094s passed
lenOfSeqSingleton data()[140] 2.988s passed
lenOfSeqConcat data()[141] 2.992s passed
lenOfSeqSub data()[142] 2.988s passed
lenOfSeqReverse data()[143] 2.988s passed
equalityToSeqGetAndSeqLenLeft data()[144] 2.990s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.008s passed
getOfSeqSingletonEQ data()[146] 2.983s passed
getOfSeqConcatEQ data()[147] 2.990s passed
getOfSeqSubEQ data()[148] 3.015s passed
getOfSeqReverseEQ data()[149] 3.034s passed
div_exists data()[14] 3.185s passed
lenOfSeqEmptyEQ data()[150] 2.993s passed
lenOfSeqSingletonEQ data()[151] 2.984s passed
lenOfSeqConcatEQ data()[152] 3.003s passed
lenOfSeqSubEQ data()[153] 2.985s passed
lenOfSeqReverseEQ data()[154] 2.982s passed
getOfSeqDefEQ data()[155] 3.002s passed
lenOfSeqDefEQ data()[156] 2.991s passed
seqConcatWithSeqEmpty1 data()[157] 2.996s passed
seqConcatWithSeqEmpty2 data()[158] 3.010s passed
seqReverseOfSeqEmpty data()[159] 2.995s passed
div_one data()[15] 3.068s passed
subSeqComplete data()[160] 3.028s passed
subSeqTailR data()[161] 3.004s passed
subSeqTailL data()[162] 3.033s passed
subSeqTailEQR data()[163] 3.004s passed
subSeqTailEQL data()[164] 3.020s passed
seqDef_split data()[165] 3.012s passed
seqDef_induction_upper data()[166] 3.046s passed
seqDef_induction_upper_concrete data()[167] 3.046s passed
seqDef_induction_lower data()[168] 3.022s passed
seqDef_induction_lower_concrete data()[169] 3.045s passed
jdiv_one data()[16] 3.033s passed
seqDef_split_in_three data()[170] 3.116s passed
seqDef_empty data()[171] 3.007s passed
seqDef_one_summand data()[172] 3.005s passed
seqDef_lower_equals_upper data()[173] 3.003s passed
seqDefOfSeq data()[174] 2.998s passed
seqSelfDefinitionEQ2 data()[175] 3.001s passed
indexOfSeqSingleton data()[176] 2.998s passed
indexOfSeqConcatFirst data()[177] 3.017s passed
indexOfSeqConcatSecond data()[178] 3.023s passed
indexOfSeqSub data()[179] 2.994s passed
div_zero data()[17] 3.214s passed
lenOfArray2seq data()[180] 3.000s passed
getAnyOfArray2seq data()[181] 3.001s passed
getOfArray2seq data()[182] 3.003s passed
getAnyOfNPermInv data()[183] 3.002s passed
seqNPermRange data()[184] 3.067s passed
seqPermTrans data()[185] 3.145s passed
seqPermRefl data()[186] 2.982s passed
seqPermSplit data()[187] 2.994s passed
seqNPermRight data()[188] 3.194s passed
seqPermFromSwap data()[189] 3.049s passed
divResZero1 data()[18] 3.048s passed
seqPermTransAlt0 data()[190] 3.005s passed
seqPermTransAlt1 data()[191] 3.006s passed
seqPermTransAlt2 data()[192] 2.988s passed
seqPermTransAlt3 data()[193] 2.998s passed
seqPermForall data()[194] 3.101s passed
seqPermExists data()[195] 3.069s passed
schiffl_lemma_2 data()[196] 20.518s passed
schiffl_thm_1 data()[197] 4.180s passed
eqSameSeq data()[198] 3.226s passed
divResZero2 data()[19] 3.011s passed
eqTermCut data()[1] 3.577s passed
divResOne1 data()[20] 3.058s passed
divResOne2 data()[21] 3.053s passed
div_cancel1 data()[22] 3.061s passed
div_cancel2 data()[23] 3.026s passed
divAddMultDenom data()[24] 3.049s passed
divMinus data()[25] 3.086s passed
divMinusDenom data()[26] 3.044s passed
divLeastDPos data()[27] 3.047s passed
divLeastDNeg data()[28] 3.031s passed
divGreatestDPos data()[29] 2.998s passed
equivAllRight data()[2] 3.365s passed
divGreatestDNeg data()[30] 3.030s passed
divIncreasingPos data()[31] 3.009s passed
divIncreasingNeg data()[32] 3.013s passed
jdiv_zero data()[33] 2.999s passed
jdivPulloutMinusNum data()[34] 3.011s passed
jdivPulloutMinusDenom data()[35] 3.034s passed
jdiv_uniquePosPos data()[36] 3.040s passed
jdiv_uniquePosNeg data()[37] 3.034s passed
jdiv_uniqueNegPos data()[38] 2.998s passed
jdiv_uniqueNegNeg data()[39] 3.052s passed
irrflConcrete1 data()[3] 3.208s passed
jdivMultDenom1 data()[40] 3.035s passed
jdivMultDenom2 data()[41] 3.014s passed
mod_geZero data()[42] 2.984s passed
mod_lessDenom data()[43] 3.004s passed
jmod_NumPos data()[44] 3.004s passed
jmod_NumNeg data()[45] 3.012s passed
jmod_geZero data()[46] 3.002s passed
jmodNumZero data()[47] 2.980s passed
jmod_pulloutminusNum data()[48] 3.020s passed
jmod_pulloutminusDenom data()[49] 2.985s passed
irrflConcrete2 data()[4] 3.148s passed
jmodUnique1 data()[50] 3.057s passed
jmodUnique2 data()[51] 3.069s passed
intDivRem data()[52] 3.004s passed
jmodjmod data()[53] 3.023s passed
jmodDivisible data()[54] 2.998s passed
jmodDivisibleRep data()[55] 2.994s passed
jdivAddMultDenom data()[56] 3.112s passed
jmodAltZero data()[57] 3.024s passed
jmodAddMultDenomZero data()[58] 2.983s passed
polyDiv_zero data()[59] 2.994s passed
cancel_gtPos data()[5] 3.182s passed
polyMod_ltdivDenom data()[60] 2.997s passed
bsum_empty data()[61] 2.967s passed
bsum_induction_upper data()[62] 2.981s passed
bsum_induction_lower data()[63] 3.005s passed
bsum_num_of_bounds data()[64] 3.010s passed
bsum_num_of_bounds2 data()[65] 2.989s passed
bsum_induction_upper2 data()[66] 2.995s passed
bsum_induction_upper_concrete data()[67] 2.973s passed
bsum_induction_upper_concrete_2 data()[68] 2.985s passed
bsum_induction_upper2_concrete data()[69] 2.997s passed
cancel_gtNeg data()[6] 3.126s passed
bsum_induction_lower_concrete data()[70] 2.970s passed
bsum_induction_lower2 data()[71] 2.987s passed
bsum_induction_lower2_concrete data()[72] 2.976s passed
bsum_positive data()[73] 3.029s passed
bsum_upper_bound data()[74] 3.013s passed
bsum_lower_bound data()[75] 3.035s passed
bsum_positive_lower_bound_element data()[76] 3.074s passed
bsum_sub_same_index data()[77] 2.995s passed
bsum_less_same_index data()[78] 3.032s passed
bsum_equal_except_one_index data()[79] 3.008s passed
moduloIntIsInInt data()[7] 3.140s passed
bsum_num_of_is_max data()[80] 3.018s passed
bsum_num_of_is_max2 data()[81] 2.991s passed
bsum_num_of_is_max3 data()[82] 3.085s passed
bsum_num_of_is_max4 data()[83] 3.019s passed
bsum_num_of_lt_max data()[84] 3.035s passed
bsum_num_of_lt_max2 data()[85] 3.021s passed
bsum_num_of_lt_max3 data()[86] 2.989s passed
bsum_num_of_lt_max4 data()[87] 3.008s passed
bsum_num_of_gt0 data()[88] 2.997s passed
bsum_num_of_gt0_alt data()[89] 3.006s passed
moduloLongIsInLong data()[8] 3.096s passed
bsum_add_concrete data()[90] 2.971s passed
bprod_all_positive data()[91] 3.016s passed
bprod_split data()[92] 2.991s passed
powConcrete0 data()[93] 2.973s passed
powConcrete1 data()[94] 2.991s passed
powSplitFactor data()[95] 2.982s passed
powAdd data()[96] 3.007s passed
powMono data()[97] 2.974s passed
powMonoConcrete data()[98] 2.988s passed
powMonoConcreteRight data()[99] 2.987s passed
moduloShortIsInShort data()[9] 3.072s passed

Standard output

742        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
767        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.11ms 
977        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1004       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)

1972       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1974       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1977       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1978       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3213       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8067       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.09s 
8136       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8166       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.3ns 
8179       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8179       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.1ns 
8183       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
10847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11746      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.08ms 
11761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.2ns 
11764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
14308      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
15126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368ns 
15128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
17554      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
18336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
18337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20696      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
20696      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
21484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.5ns 
21485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
23813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.15ms 
24666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
24667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
27004      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27784      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.79ms 
27807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.4ns 
27808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
30174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30945      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 657.5ns 
30948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.7ns 
30949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
33286      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34039      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34041      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.2ns 
34043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.8ns 
34044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
36346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37113      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 510.4ns 
37115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 
37116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
39407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.4ns 
40141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 
40142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42428      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
42428      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.9ns 
43181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.1ns 
43182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
45480      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46246      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.46ms 
46249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.78ms 
46252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48532      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
48532      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49336      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.76ms 
49344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49344      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.3ns 
49345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
51626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
52526      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.43ms 
52529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
52529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
52530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
54838      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
55589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
55595      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
55597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
55598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.6ns 
55599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
57879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
58625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
58628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
58630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
58630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 
58631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
60953      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
61791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
61842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.97ms 
61844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
61845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
61846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
64129      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
64876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
64891      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.94ms 
64893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
64893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.4ns 
64894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67168      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
67168      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
67889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
67902      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
67904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
67904      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
67905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
70198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
70938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
70960      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.77ms 
70961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
70962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.2ns 
70963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
73246      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
73992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
74011      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.17ms 
74018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
74020      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.84ms 
74021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
76310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
77053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
77077      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.08ms 
77079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
77079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
77080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
79362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
80100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
80103      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
80104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
80104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
80105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82371      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
82371      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
83113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
83152      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.87ms 
83154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
83154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
83155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
85431      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
86179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
86238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.17ms 
86239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
86239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
86240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88518      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
88518      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
89238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
89282      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.69ms 
89283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
89283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
89284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
91587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
92323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
92330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
92331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
92331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
92332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
94610      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
95348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
95360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
95361      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
95361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
95362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97613      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
97613      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
98348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
98358      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
98360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
98360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
98361      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
100632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
101376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
101384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
101390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
101390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
101391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
103654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
104390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
104398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
104399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
104399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
104400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
106669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
107404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
107411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
107412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
107412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
107413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
109670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
110406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
110410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
110412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
110412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.6ns 
110413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
112675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
113410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
113420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
113422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
113422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
113423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
115687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
116404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
116454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.7ms 
116456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
116456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.5ns 
116457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
118736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
119473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
119494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.76ms 
119498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
119498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
119499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
121779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
122514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
122531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
122533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
122533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
122534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
124778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
125513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
125530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
125531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
125531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
125532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
127789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
128565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
128581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
128583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
128584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.7ns 
128585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
130828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
131571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
131614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.87ms 
131618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
131619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
131619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
133886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
134625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
134630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
134632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
134633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
134634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
136894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
137611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
137615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
137617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
137617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250ns 
137618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
139878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
140612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
140620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
140621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
140621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
140622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
142891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
143615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
143623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
143625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
143625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.6ns 
143626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
145883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
146616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
146635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.57ms 
146636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
146637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.7ns 
146637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
148896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
149630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
149637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
149639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
149639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
149639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
151880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
152615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
152618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
152619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
152619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
152620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
154895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
155635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
155639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
155640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
155640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
155640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
157877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
158621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
158625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
158627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
158627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
158628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
160884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
161617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
161683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.41ms 
161684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
161684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
161685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
163950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
164665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
164751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.63ms 
164753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
164753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.5ns 
164754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
167015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
167752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
167755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
167756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
167756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
167757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
170014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
170745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
170778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.51ms 
170780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
170781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.5ns 
170782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
173017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
173749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
173777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms 
173778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
173778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
173779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
176033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
176768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
176770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
176772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
176772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
176773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
179005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
179744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
179882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127ms 
179884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
179884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137ns 
179885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
182153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
182895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
182906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
182907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
182908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.3ns 
182908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
185168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
185882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
185890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
185891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
185891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
185891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
188137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
188868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
188883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.68ms 
188884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
188885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
188885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
191137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
191869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
191880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
191881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
191882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
191882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
194115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
194844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
194848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
194849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
194849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
194850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
197093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
197825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
197829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
197831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
197831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
197831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
200078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
200812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
200833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
200835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
200835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
200835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
203095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
203828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
203844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 
203845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
203845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
203846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
206104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
206819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
206833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms 
206835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
206835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 
206836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
209094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
209826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
209829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
209830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
209830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
209831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
212085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
212798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
212803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
212804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
212804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
212804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
215050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
215781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
215787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
215788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
215788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
215789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
218050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
218782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
218785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
218786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
218786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
218787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
221022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
221754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
221756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.4ns 
221757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
221757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
221758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
224008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
224740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
224743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
224744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
224744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
224745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
226984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
227716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
227718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.8ns 
227720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
227720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
227721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
229969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
230700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
230744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.51ms 
230749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
230750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.2ns 
230751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
233010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
233725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
233760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.61ms 
233762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
233763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.4ns 
233764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
236027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
236764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
236796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.5ms 
236797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
236797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
236798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
239060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
239774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
239869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.91ms 
239871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
239871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
239871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
242105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
242837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
242865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.54ms 
242866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
242867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
242867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
245118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
245850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
245898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.63ms 
245899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
245899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
245900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
248147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
248879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
248905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.01ms 
248906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
248907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
248907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
251171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
251904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
251923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.77ms 
251925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
251925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
251925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
254175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
254891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
254915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.6ms 
254916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
254916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
254917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
257251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
257982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
258000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.66ms 
258001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
258002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
258002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
260256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
260969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
261020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.68ms 
261021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
261021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
261022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
263296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
264031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
264054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.81ms 
264055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
264056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
264056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
266316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
267052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
267075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.35ms 
267076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
267076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
267077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
269309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
270041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
270064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.54ms 
270066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
270066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
270066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
272321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
273052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
273072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.09ms 
273073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
273073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
273074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
275332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
276044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
276070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
276071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
276071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
276071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
278319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
279052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
279076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
279077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
279077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
279078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
281325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
282040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
282047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
282048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
282048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
282049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
284311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
285045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
285062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.09ms 
285063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
285063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
285064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
287315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
288050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
288054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
288055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
288055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.7ns 
288055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
290292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
291025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
291027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.9ns 
291028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
291028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
291029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
293277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
294015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
294019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.9ns 
294020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
294020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
294021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
296259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
296995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
297001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
297002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
297002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
297003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
299269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
300001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
300007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
300009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
300009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 
300010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
302257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
302971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
302982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.96ms 
302983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
302983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
302984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
305235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
305967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
305970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
305971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
305971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
305972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
308224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
308955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
308957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.2ns 
308958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
308958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
308959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
311192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
311924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
311929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
311930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
311930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
311931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
314186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
314917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
314919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.9ns 
314920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
314920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
314921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
317173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
317890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
317891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.7ns 
317893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
317893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
317893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
320141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
320873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
320875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.9ns 
320876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
320876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
320876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
323135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
323868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
323871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
323872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
323872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
323873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
326124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
326839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
326852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.76ms 
326854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
326854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 
326855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
329106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
329843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
329847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
329848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
329848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
329849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
332100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
332835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
332842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
332843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
332843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
332843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
335090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
335805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
335809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
335810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
335810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
335811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
338083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
338816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
338832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms 
338833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
338833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
338834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
341082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
341815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
341818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
341819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
341819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
341820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
344068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
344801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
344804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
344805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
344805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
344805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
347039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
347773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
347777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
347778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
347778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
347778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
350027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
350762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
350778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
350780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
350780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 
350781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
353026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
353758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
353762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.5ns 
353763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
353763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
353764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
356005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
356734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
356771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.95ms 
356773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
356773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
356773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
359030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
359745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
359748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
359749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
359749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
359750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
361996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
362734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
362756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.35ms 
362758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
362758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
362759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
365013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
365746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
365765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ms 
365766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
365766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
365767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
368021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
368758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
368781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.79ms 
368782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
368782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
368783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
371050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
371786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
371788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553ns 
371791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
371791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
371792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
374043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
374776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
374781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
374782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
374782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
374783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
377030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
377768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
377771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
377772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
377772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
377773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
380025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
380742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
380744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.8ns 
380746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
380746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.8ns 
380748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
382992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
383728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
383730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.4ns 
383731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
383731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
383732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
385976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
386713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
386715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
386717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
386717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
386717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
388959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
389696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
389699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
389700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
389700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
389701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
391954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
392692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
392701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
392702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
392703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
392703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
394949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
395687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
395699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
395700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
395700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
395701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
397941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
398677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
398687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.96ms 
398688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
398688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
398689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
400934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
401675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
401692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
401693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
401694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.3ns 
401694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
403944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
404685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
404690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
404691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
404691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
404691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
406938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
407678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
407683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
407684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
407684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
407685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
409929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
410669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
410671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.2ns 
410672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
410672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
410673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
412914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
413657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
413660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
413662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
413662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns 
413663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
415914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
416655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
416657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 837ns 
416658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
416658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
416659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
418901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
419641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
419652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
419653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
419653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
419653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
421895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
422634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
422637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
422639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
422639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
422639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
424898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
425641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
425647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
425648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
425648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
425648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
427901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
428640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
428642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.6ns 
428643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
428643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
428644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
430887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
431628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
431630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.5ns 
431631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
431631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
431632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
433877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
434619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
434623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
434624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
434624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
434625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
436868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
437607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
437610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
437611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
437611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
437612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
439856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
440596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
440599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
440600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
440600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
440600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
442847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
443586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
443588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
443589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
443589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
443590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
445853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
446591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
446596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
446597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
446598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
446598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
448839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
449578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
449580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
449581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
449581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
449582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
451821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
452560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
452571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
452572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
452572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.9ns 
452573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
454845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
455583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
455585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 575.8ns 
455586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
455586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
455587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
457851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
458612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
458619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
458620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
458621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
458621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
460871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
461610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
461613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.3ns 
461614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
461614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.6ns 
461615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
463855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
464595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
464597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.4ns 
464598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
464598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
464599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
466859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
467596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
467600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
467601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
467601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
467602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
469844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
470583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
470586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
470587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
470587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
470588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
472825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
473565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
473568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
473569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
473569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
473570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
475828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
476566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
476569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
476572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
476572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
476572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
478816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
479557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
479561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
479562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
479562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
479563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
481804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
482544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
482557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
482558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
482558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
482559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
484815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
485553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
485568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
485569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
485569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
485570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
487810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
488553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
488563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
488564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
488564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
488565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
490842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
491580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
491590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
491591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
491591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
491592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
493833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
494571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
494595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.17ms 
494596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
494596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
494597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
496864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
497603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
497627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.05ms 
497628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
497628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
497629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
499870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
500609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
500632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.76ms 
500633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
500633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
500634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
502900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
503638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
503651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
503653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
503653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
503653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
505894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
506633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
506663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.98ms 
506665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
506665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
506665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
508924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
509664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
509709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.84ms 
509710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
509711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
509711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
511979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
512719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
512755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.91ms 
512756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
512756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
512757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
514998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
515738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
515777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.58ms 
515779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
515779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
515779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
518039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
518780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
518822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.84ms 
518823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
518823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
518824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
521069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
521826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
521938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.1ms 
521939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
521939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
521940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
524191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
524933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
524944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
524947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
524947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
524948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
527206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
527944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
527951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
527952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
527952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
527952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
530210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
530949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
530954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
530955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
530955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
530956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
533197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
533935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
533952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms 
533953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
533953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
533954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
536204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
536942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
536953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
536954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
536954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
536955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
539209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
539948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
539951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
539952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
539952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
539953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
542213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
542952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
542967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
542968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
542968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
542969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
545213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
545975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
545990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
545992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
545992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
545992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
548227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
548967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
548985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.29ms 
548986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
548986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
548987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
551243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
551982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
551984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
551986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
551986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
551986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
554241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
554982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
554985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
554986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
554986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
554987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
557244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
557982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
557988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
557989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
557989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
557990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
560245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
560984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
560990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
560991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
560991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
560992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
563250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
563992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
564057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.73ms 
564059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
564059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
564059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
566376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
567176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
567202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.47ms 
567204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
567204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
567205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
569427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
570162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
570186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.42ms 
570187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
570187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
570188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
572437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
573178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
573179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 239.8ns 
573181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
573181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
573182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
575428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
576187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
576373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.07ms 
576374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
576374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
576375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
578626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
579374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
579422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.42ms 
579424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
579424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.6ns 
579425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
581684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
582426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
582428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.4ns 
582429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
582429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
582430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
584690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
585432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
585433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 293.8ns 
585434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
585435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
585435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
587678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
588420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
588421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312ns 
588423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
588423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
588423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
590676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
591417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
591419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 420ns 
591420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
591420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
591421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
593681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
594422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
594519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.94ms 
594522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
594522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 
594524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
596783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
597546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
597589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.89ms 
597590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
597590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
597591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
599846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
600587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
600588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
600612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
600647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
600663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
600667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
600672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
600675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
600676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
600678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
600680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
600682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
600684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
600685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
600845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
600846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
600847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
600849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
600850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
600948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
600949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
600950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
600951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
600952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
600953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
601113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
601115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
601116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
601118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
601119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
601122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
601275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
601276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
601277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
601277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
601278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
601279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
601285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
601286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
601287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
601288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
601289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
601290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
601297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
601297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
601299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
601300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
601300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
601301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
601429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
601430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
601431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
601552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
601553     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)'' 
601555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
601556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
601558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
601558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
601559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
601560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
601564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
601565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
601566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
601567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
601568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
601679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
601683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
601684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
601685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
601685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
601686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
601687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
601813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
601814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
601815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
601817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
601817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
601818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
601819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
601820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
601909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
601910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
602021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
602027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
602033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
602034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
602035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
602036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
602039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
602039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
602040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
602041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
602053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
602063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
602172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
602173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
602175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
602176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
602176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
602177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
602179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
602180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
602232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
602238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
602323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
602324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
602325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
602327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
602327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
602328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
602435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
602438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
602441     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)'' 
602442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
602443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
602447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
602447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
602448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
602455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
602460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
602462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
602462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
602542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
602544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
602544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
602545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
602546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
602547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
602638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
602639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
602640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
602641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
602641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
602642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
602642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
602643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
602715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
602716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
602783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
602783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
602783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
602787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
602790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
602794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
602902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
602903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
602903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
602904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
602913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
602986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
606275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
606275     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)'' 
606281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
606282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
606282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
606283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
606283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
606290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
606292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
606293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
606294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
606294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
606378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
606382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
606383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
606383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
606384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
606385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
606385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
606471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
606472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
606473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
606474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
606475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
606476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
606476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
606477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
606580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
606582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
606648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
606652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
606656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
606657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
606657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
606658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
606667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
606738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
606739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
606740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
606741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
606806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
606814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
606814     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)'' 
606816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
606817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
606817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
606818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
606818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
606827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
606828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
606829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
606830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
606830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
606909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
606910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
606911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
606912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
606912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
606994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
606997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
606998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
606999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
606999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
607000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
607000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
607088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
607089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
607090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
607091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
607091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
607092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
607092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
607093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
607094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
607094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
607095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
607096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
607096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
607096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
607097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
607176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
607177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
607182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
607253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
607325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
607326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
607327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
607328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
607328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
607329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
607329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
607329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
607330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
607407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
607413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
607494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
607495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
607495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
607496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
607497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
607497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
607497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
607498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
607502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
607503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
607578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
607583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
607588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
607677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
607678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
607679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
607680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
607680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
607680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
607680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
607681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
607730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
607731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
607732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
607732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
607733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
607738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
607742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
607847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
607962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
607963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
607964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
607964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
608116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
608196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
608197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
611007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
611012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
611013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
611013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
611014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
611117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
611119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
611120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
611120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
611121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
611216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
613987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
616939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
616944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
616945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
616945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
616946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
617049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
617051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
617051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
617052     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)' ...' 
617054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
618108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
618108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
618109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
620608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
621383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
621385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 
621385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
621415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
621429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
621432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
621434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
621435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
621441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
621442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
621446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
621449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
621450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
621460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
621462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
621462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
621529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
621540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
621541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
621542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
621542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
621658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
621659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
621660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
621661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
621661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
621664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
621673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
621673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
621674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
621675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
621676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
621794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
621795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
621796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
621797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
621798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
621798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
621892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
621901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
621902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
621903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
621903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
621905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
621905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
621906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
621907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
621907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
621917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
621918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
621918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
621919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
621919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
621920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
621920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
621921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
621922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
621925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
621995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
621997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
622042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
622043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
622044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
622046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
622046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
622047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
622092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
622101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
622102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
622103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
622104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
622109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
622110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
622190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
622192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
622195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
622241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
622289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
622289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 
622290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
624728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
625484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
625514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.85ms