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

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

tests
0

failures
0

ignored
10m34.05s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.077s passed
powPositiveConcrete data()[101] 3.053s passed
powGeq1Concrete data()[102] 3.042s passed
pow2InIntLower data()[103] 3.063s passed
pow2InIntUpper data()[104] 3.049s passed
logSelfConcrete data()[105] 3.054s passed
log1Concrete data()[106] 3.086s passed
logProduct data()[107] 3.050s passed
logTimesBaseConcrete data()[108] 3.059s passed
logProdIdentity data()[109] 3.071s passed
moduloByteIsInByte data()[10] 3.134s passed
logProdIdentityConcrete data()[110] 3.052s passed
logPowIdentity data()[111] 3.067s passed
logPowIdentityConcrete data()[112] 3.047s passed
logPositive data()[113] 3.069s passed
logPositiveConcrete data()[114] 3.057s passed
logMono data()[115] 3.089s passed
logMonoConcrete data()[116] 3.042s passed
powLogLess data()[117] 3.062s passed
powLogMore2 data()[118] 3.088s passed
logLessThanPow data()[119] 3.076s passed
moduloCharIsInChar data()[11] 3.155s passed
logLessThanPowConcrete data()[120] 3.068s passed
logSqueeze data()[121] 3.070s passed
ifthenelse_equals data()[122] 3.065s passed
ifthenelse_equals_1 data()[123] 3.086s passed
ifthenelse_equals_2 data()[124] 3.067s passed
disjointWithSingleton1 data()[125] 3.087s passed
disjointWithSingleton2 data()[126] 3.053s passed
disjointArrayRanges data()[127] 3.097s passed
disjointArrayRangeAllFields1 data()[128] 3.059s passed
disjointArrayRangeAllFields2 data()[129] 3.088s passed
div_unique1 data()[12] 3.159s passed
seqSelfDefinition data()[130] 3.080s passed
seqOutsideValue data()[131] 3.060s passed
castedGetAny data()[132] 3.077s passed
seqGetAlphaCast data()[133] 3.078s passed
getOfSeqSingleton data()[134] 3.066s passed
getOfSeqSingletonConcrete data()[135] 3.072s passed
getOfSeqConcat data()[136] 3.076s passed
getOfSeqSub data()[137] 3.060s passed
getOfSeqReverse data()[138] 3.083s passed
lenOfSeqEmpty data()[139] 3.073s passed
div_unique2 data()[13] 3.138s passed
lenOfSeqSingleton data()[140] 3.073s passed
lenOfSeqConcat data()[141] 3.054s passed
lenOfSeqSub data()[142] 3.076s passed
lenOfSeqReverse data()[143] 3.069s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.078s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.046s passed
getOfSeqSingletonEQ data()[146] 3.066s passed
getOfSeqConcatEQ data()[147] 3.072s passed
getOfSeqSubEQ data()[148] 3.070s passed
getOfSeqReverseEQ data()[149] 3.076s passed
div_exists data()[14] 3.388s passed
lenOfSeqEmptyEQ data()[150] 3.069s passed
lenOfSeqSingletonEQ data()[151] 3.045s passed
lenOfSeqConcatEQ data()[152] 3.068s passed
lenOfSeqSubEQ data()[153] 3.077s passed
lenOfSeqReverseEQ data()[154] 3.068s passed
getOfSeqDefEQ data()[155] 3.069s passed
lenOfSeqDefEQ data()[156] 3.073s passed
seqConcatWithSeqEmpty1 data()[157] 3.072s passed
seqConcatWithSeqEmpty2 data()[158] 3.079s passed
seqReverseOfSeqEmpty data()[159] 3.078s passed
div_one data()[15] 3.106s passed
subSeqComplete data()[160] 3.074s passed
subSeqTailR data()[161] 3.091s passed
subSeqTailL data()[162] 3.100s passed
subSeqTailEQR data()[163] 3.096s passed
subSeqTailEQL data()[164] 3.088s passed
seqDef_split data()[165] 3.096s passed
seqDef_induction_upper data()[166] 3.111s passed
seqDef_induction_upper_concrete data()[167] 3.123s passed
seqDef_induction_lower data()[168] 3.119s passed
seqDef_induction_lower_concrete data()[169] 3.119s passed
jdiv_one data()[16] 3.118s passed
seqDef_split_in_three data()[170] 3.173s passed
seqDef_empty data()[171] 3.082s passed
seqDef_one_summand data()[172] 3.089s passed
seqDef_lower_equals_upper data()[173] 3.072s passed
seqDefOfSeq data()[174] 3.080s passed
seqSelfDefinitionEQ2 data()[175] 3.077s passed
indexOfSeqSingleton data()[176] 3.062s passed
indexOfSeqConcatFirst data()[177] 3.099s passed
indexOfSeqConcatSecond data()[178] 3.084s passed
indexOfSeqSub data()[179] 3.085s passed
div_zero data()[17] 3.132s passed
lenOfArray2seq data()[180] 3.093s passed
getAnyOfArray2seq data()[181] 3.083s passed
getOfArray2seq data()[182] 3.072s passed
getAnyOfNPermInv data()[183] 3.102s passed
seqNPermRange data()[184] 3.136s passed
seqPermTrans data()[185] 3.104s passed
seqPermRefl data()[186] 3.107s passed
seqPermSplit data()[187] 3.074s passed
seqNPermRight data()[188] 3.279s passed
seqPermFromSwap data()[189] 3.126s passed
divResZero1 data()[18] 3.110s passed
seqPermTransAlt0 data()[190] 3.110s passed
seqPermTransAlt1 data()[191] 3.068s passed
seqPermTransAlt2 data()[192] 3.086s passed
seqPermTransAlt3 data()[193] 3.066s passed
seqPermForall data()[194] 3.182s passed
seqPermExists data()[195] 3.174s passed
schiffl_lemma_2 data()[196] 22.816s passed
schiffl_thm_1 data()[197] 3.895s passed
eqSameSeq data()[198] 3.180s passed
divResZero2 data()[19] 3.119s passed
eqTermCut data()[1] 3.793s passed
divResOne1 data()[20] 3.115s passed
divResOne2 data()[21] 3.097s passed
div_cancel1 data()[22] 3.143s passed
div_cancel2 data()[23] 3.088s passed
divAddMultDenom data()[24] 3.108s passed
divMinus data()[25] 3.159s passed
divMinusDenom data()[26] 3.146s passed
divLeastDPos data()[27] 3.116s passed
divLeastDNeg data()[28] 3.097s passed
divGreatestDPos data()[29] 3.072s passed
equivAllRight data()[2] 3.455s passed
divGreatestDNeg data()[30] 3.102s passed
divIncreasingPos data()[31] 3.087s passed
divIncreasingNeg data()[32] 3.091s passed
jdiv_zero data()[33] 3.087s passed
jdivPulloutMinusNum data()[34] 3.071s passed
jdivPulloutMinusDenom data()[35] 3.148s passed
jdiv_uniquePosPos data()[36] 3.086s passed
jdiv_uniquePosNeg data()[37] 3.072s passed
jdiv_uniqueNegPos data()[38] 3.093s passed
jdiv_uniqueNegNeg data()[39] 3.070s passed
irrflConcrete1 data()[3] 3.403s passed
jdivMultDenom1 data()[40] 3.095s passed
jdivMultDenom2 data()[41] 3.091s passed
mod_geZero data()[42] 3.067s passed
mod_lessDenom data()[43] 3.088s passed
jmod_NumPos data()[44] 3.111s passed
jmod_NumNeg data()[45] 3.079s passed
jmod_geZero data()[46] 3.088s passed
jmodNumZero data()[47] 3.061s passed
jmod_pulloutminusNum data()[48] 3.060s passed
jmod_pulloutminusDenom data()[49] 3.080s passed
irrflConcrete2 data()[4] 3.223s passed
jmodUnique1 data()[50] 3.157s passed
jmodUnique2 data()[51] 3.135s passed
intDivRem data()[52] 3.076s passed
jmodjmod data()[53] 3.083s passed
jmodDivisible data()[54] 3.097s passed
jmodDivisibleRep data()[55] 3.057s passed
jdivAddMultDenom data()[56] 3.193s passed
jmodAltZero data()[57] 3.123s passed
jmodAddMultDenomZero data()[58] 3.057s passed
polyDiv_zero data()[59] 3.072s passed
cancel_gtPos data()[5] 3.192s passed
polyMod_ltdivDenom data()[60] 3.097s passed
bsum_empty data()[61] 3.060s passed
bsum_induction_upper data()[62] 3.072s passed
bsum_induction_lower data()[63] 3.079s passed
bsum_num_of_bounds data()[64] 3.070s passed
bsum_num_of_bounds2 data()[65] 3.081s passed
bsum_induction_upper2 data()[66] 3.061s passed
bsum_induction_upper_concrete data()[67] 3.065s passed
bsum_induction_upper_concrete_2 data()[68] 3.079s passed
bsum_induction_upper2_concrete data()[69] 3.046s passed
cancel_gtNeg data()[6] 3.278s passed
bsum_induction_lower_concrete data()[70] 3.054s passed
bsum_induction_lower2 data()[71] 3.075s passed
bsum_induction_lower2_concrete data()[72] 3.048s passed
bsum_positive data()[73] 3.131s passed
bsum_upper_bound data()[74] 3.079s passed
bsum_lower_bound data()[75] 3.074s passed
bsum_positive_lower_bound_element data()[76] 3.117s passed
bsum_sub_same_index data()[77] 3.108s passed
bsum_less_same_index data()[78] 3.094s passed
bsum_equal_except_one_index data()[79] 3.104s passed
moduloIntIsInInt data()[7] 3.149s passed
bsum_num_of_is_max data()[80] 3.081s passed
bsum_num_of_is_max2 data()[81] 3.088s passed
bsum_num_of_is_max3 data()[82] 3.080s passed
bsum_num_of_is_max4 data()[83] 3.071s passed
bsum_num_of_lt_max data()[84] 3.088s passed
bsum_num_of_lt_max2 data()[85] 3.081s passed
bsum_num_of_lt_max3 data()[86] 3.090s passed
bsum_num_of_lt_max4 data()[87] 3.085s passed
bsum_num_of_gt0 data()[88] 3.070s passed
bsum_num_of_gt0_alt data()[89] 3.087s passed
moduloLongIsInLong data()[8] 3.149s passed
bsum_add_concrete data()[90] 3.057s passed
bprod_all_positive data()[91] 3.062s passed
bprod_split data()[92] 3.078s passed
powConcrete0 data()[93] 3.058s passed
powConcrete1 data()[94] 3.044s passed
powSplitFactor data()[95] 3.074s passed
powAdd data()[96] 3.043s passed
powMono data()[97] 3.081s passed
powMonoConcrete data()[98] 3.048s passed
powMonoConcreteRight data()[99] 3.045s passed
moduloShortIsInShort data()[9] 3.152s passed

Standard output

567        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
589        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.79ms 
811        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848        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)

1940       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1943       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1946       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1947       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3353       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8428       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.62s 
8487       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8519       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.6ns 
8530       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8530       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
8535       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
11393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12314      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.92ms 
12326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12326      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.2ns 
12328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
14889      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15778      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.08ms 
15782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.1ns 
15785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
18330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19180      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
19186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
19187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
21599      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22407      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
22409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22409      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.5ns 
22410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
24799      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.74ms 
25602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25602      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.4ns 
25603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
28026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28876      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.41ms 
28880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.7ns 
28882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
31237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32027      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.21ns 
32030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.8ns 
32031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
34397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35176      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.91ns 
35178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.4ns 
35179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
37549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38327      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.61ns 
38330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.3ns 
38332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
40686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41462      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.51ns 
41465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 
41466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43842      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43843      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44616      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.71ns 
44620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.1ns 
44621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
46957      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.27ms 
47785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.11ns 
47787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
50138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50917      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.8ms 
50920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348ns 
50922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
53305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54304      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 215.42ms 
54308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.61ns 
54310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
56635      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57412      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
57414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
57415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
59749      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60530      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
60533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.8ns 
60535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
62852      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.05ms 
63665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63665      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.5ns 
63666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65994      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
65994      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.13ms 
66774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
66775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
69108      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69892      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
69895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.2ns 
69897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
72221      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73007      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
73008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
73009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
75347      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76104      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms 
76106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76106      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
76107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
78452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79222      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79247      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.79ms 
79248      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
79249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
81569      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82335      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
82337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.5ns 
82338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84665      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84665      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85442      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.6ms 
85445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85445      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 
85446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
87786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88602      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.9ms 
88604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88604      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.8ns 
88605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
90908      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91747      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.82ms 
91753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.9ms 
91757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
94096      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94865      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
94866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
94868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97187      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
97187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97961      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.52ms 
97963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
97964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
100285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
101036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
101037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
103361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
104137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
104138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
106446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
107225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124ns 
107226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
109567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
110316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
110316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
112639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
113403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
113404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
115696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
116474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
116475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
118799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.71ms 
119623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.9ns 
119624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
121926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
122709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.9ns 
122710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
125001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
125779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
125780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
128097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
128873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
128874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
131166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 
131942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
131943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
134260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.91ms 
135037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
135038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
137364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
138129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
138129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
140426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
141198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.1ns 
141203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
143542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
144285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
144286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
146621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
147396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
147397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
149683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.39ms 
150484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.1ns 
150485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
152803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.01ms 
153571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
153572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
155867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
156628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
156631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
156633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
156633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.3ns 
156634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
158953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
159687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
159692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
159693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
159693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
159694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
162010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
162767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
162771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
162775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
162775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.9ns 
162777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
165072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
165838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
165929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.63ms 
165936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
165936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.7ns 
165937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
168257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
168990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.51ms 
169071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
169071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
171381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
172147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.11ns 
172149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
174437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.44ms 
175230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.31ns 
175232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
177543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
178296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
178325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.49ms 
178327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
178328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.2ns 
178329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
180623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
181379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
181382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
181384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
181384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
181385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
183696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
184434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
184575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.24ms 
184577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
184577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
184578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
186927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
187687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
187698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
187700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
187700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
187701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
189991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
190747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
190755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
190758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
190758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.2ns 
190759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
193080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
193812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
193828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
193829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
193830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
193830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
196149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
196907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
196924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
196926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
196926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
196927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
199229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
199981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
199985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
199986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
199986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
199987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
202294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
203051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
203056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
203060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
203060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.4ns 
203061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
205360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
206114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 
206139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
206139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
208436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
209191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
209207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
209209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
209209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
209210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
211518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
212273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
212289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
212290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
212290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
212291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
214592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
215346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
215349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
215351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
215351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
215351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
217676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
218410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
218414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
218417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
218417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
218418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
220733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
221488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
221494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
221495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
221495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
221496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
223782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
224537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
224540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
224541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
224541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
224542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
226853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
227591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
227593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 768.51ns 
227596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
227596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.1ns 
227597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
229910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
230665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
230669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
230670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
230671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
230671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
232963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
233714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
233717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 968.01ns 
233718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
233718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
233719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
236026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
236802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
236848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.25ms 
236850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
236850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.1ns 
236851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
239141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
239896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
239927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.05ms 
239929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
239929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
239930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
242239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
242972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
243001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.57ms 
243003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
243003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
243004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
245315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
246075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
246117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.44ms 
246120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
246121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 821.91ns 
246122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
248441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
249197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
249226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms 
249227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
249227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
249228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
251542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
252272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
252320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.46ms 
252322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
252322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
252323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
254645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
255399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
255424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.88ms 
255426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
255426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
255426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
257718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
258486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
258506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
258507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
258507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
258508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
260815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
261569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
261593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.37ms 
261594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
261594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
261595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
263895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
264654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
264673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
264674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
264674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
264675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
266987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
267718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
267744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
267746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
267746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
267747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
270054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
270808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
270832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms 
270834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
270834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
270835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
273126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
273880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
273913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.5ms 
273916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
273916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.5ns 
273918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
276248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
276979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
277003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.25ms 
277004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
277005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
277005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
279314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
280068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
280089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
280090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
280090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
280091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
282380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
283134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
283158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.78ms 
283159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
283159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
283160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
285469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
286221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
286246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
286247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
286247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
286248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
288541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
289295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
289302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
289303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
289303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
289304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
291612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
292347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
292364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.39ms 
292365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
292365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
292366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
294682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
295438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
295442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
295443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
295443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
295444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
297742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
298498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
298501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.31ns 
298502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
298502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
298503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
300811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
301542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
301544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.21ns 
301545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
301545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
301546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
303858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
304612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
304618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
304619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
304620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
304620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
306902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
307656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
307662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
307663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
307663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
307664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
309971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
310731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
310743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
310744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
310744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
310745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
313032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
313787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
313791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
313792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
313792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
313792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
316079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
316833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
316835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.91ns 
316836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
316836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
316837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
319147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
319904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
319912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
319914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
319915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.5ns 
319916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
322210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
322963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
322965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.91ns 
322966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
322966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
322967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
325275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
326005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
326007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.81ns 
326009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
326009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
326009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
328315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
329069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
329071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.41ns 
329072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
329072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
329073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
331360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
332116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
332120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
332121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
332121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
332122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
334433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
335164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
335173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
335174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
335174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
335175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
337500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
338255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
338259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
338260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
338260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
338261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
340550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
341303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
341309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
341311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
341311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
341311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
343613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
344364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
344368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
344369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
344369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
344370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
346663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
347417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
347440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 
347441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
347441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
347442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
349753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
350488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
350492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
350493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
350493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
350494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
352801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
353555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
353558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
353560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
353560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
353560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
355847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
356601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
356605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
356606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
356606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
356607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
358906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
359658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
359674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
359675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
359675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
359676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
361972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
362726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
362730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.01ns 
362732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
362732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
362733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
365030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
365780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
365821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.36ms 
365822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
365822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
365823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
368104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
368859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
368863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
368864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
368864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
368865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
371173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
371903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
371924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.43ms 
371926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
371926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
371927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
374232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
374986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
375011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
375014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
375014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.3ns 
375015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
377330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
378065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
378089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.04ms 
378090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
378090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
378091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
380396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
381154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
381156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.81ns 
381157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
381157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
381158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
383463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
384221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
384226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
384228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
384228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
384228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
386530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
387288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
387292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
387293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
387293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
387294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
389614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
390374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
390377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.21ns 
390379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
390379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.1ns 
390380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
392679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
393442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
393445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.21ns 
393446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
393446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
393447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
395766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
396528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
396531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
396532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
396533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
396533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
398821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
399582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
399585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
399586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
399586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
399587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
401912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
402672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
402682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
402683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
402683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
402684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
404987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
405725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
405736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
405744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
405744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.7ns 
405745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
408051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
408817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
408829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
408832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
408832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 
408833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
411138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
411899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
411911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
411912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
411912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
411913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
414198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
414966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
414971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
414972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
414972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
414973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
417277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
418042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
418048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
418049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
418049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
418050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
420359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
421123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
421125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.41ns 
421127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
421127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
421127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
423425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
424188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
424191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
424192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
424192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
424193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
426498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
427260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
427263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 835.31ns 
427265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
427265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.7ns 
427266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
429568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
430329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
430340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
430341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
430341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
430342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
432655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
433395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
433399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
433400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
433401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
433401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
435708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
436476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
436482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
436483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
436483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
436484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
438791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
439553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
439555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.61ns 
439556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
439556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
439557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
441863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
442626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
442628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.01ns 
442630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
442630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
442630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
444917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
445678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
445682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
445684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
445685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.3ns 
445685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
447992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
448756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
448758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
448760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
448760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
448760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
451064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
451825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
451828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
451829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
451829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
451830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
454139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
454902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
454905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
454906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
454906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
454907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
457207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
457947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
457952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
457953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
457953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
457954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
460254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
461015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
461017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
461019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
461019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
461020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
463316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
464078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
464089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
464090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
464090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
464091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
466396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
467157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
467159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.71ns 
467161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
467161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
467161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
469467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
470228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
470235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
470237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
470237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
470237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
472539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
473302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
473305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 915.61ns 
473306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
473306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
473306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
475604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
476347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
476349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.81ns 
476350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
476350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
476351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
478651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
479412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
479417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
479418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
479418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
479419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
481732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
482491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
482494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
482495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
482495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
482496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
484796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
485559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
485562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
485563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
485563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
485564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
487866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
488628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
488632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
488633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
488633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
488634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
490936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
491699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
491704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
491705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
491705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
491706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
494001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
494762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
494776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms 
494777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
494778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
494778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
497078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
497840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
497855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
497857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
497857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
497857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
500156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
500921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
500934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ms 
500935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
500935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
500936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
503237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
503997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
504007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
504009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
504009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
504009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
506311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
507074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
507098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
507100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
507100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
507101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
509410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
510173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
510198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
510200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
510200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
510200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
512506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
513271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
513294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
513296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
513296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
513297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
515605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
516369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
516383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
516384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
516384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
516385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
518684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
519446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
519478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.32ms 
519481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
519481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.1ns 
519482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
521782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
522545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
522590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.84ms 
522591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
522591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
522592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
524913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
525676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
525713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.6ms 
525714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
525714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
525715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
528022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
528786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
528832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.77ms 
528834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
528834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.4ns 
528835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
531147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
531909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
531951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.61ms 
531953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
531953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
531954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
534249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
535010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
535124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.52ms 
535126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
535126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
535127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
537437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
538199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
538206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
538208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
538208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
538209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
540527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
541288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
541296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
541297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
541297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
541298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
543600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
544362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
544367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
544368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
544369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
544369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
546667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
547430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
547448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
547449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
547449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
547450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
549746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
550510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
550524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
550525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
550526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
550526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
552823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
553583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
553587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
553588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
553588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
553589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
555907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
556668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
556685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 
556686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
556686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
556687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
558991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
559753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
559769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
559770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
559770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
559771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
562072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
562836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
562854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
562856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
562856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.3ns 
562857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
565180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
565944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
565947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
565948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
565948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
565949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
568263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
569027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
569031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
569032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
569032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
569033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
571332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
572095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
572102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
572104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
572104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.9ns 
572105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
574436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
575197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
575204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
575205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
575205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
575206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
577511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
578274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
578340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.07ms 
578342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
578343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.5ns 
578343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
580656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
581418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
581444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.88ms 
581446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
581446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
581446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
583769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
584530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
584552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.11ms 
584553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
584553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
584554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
586859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
587624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
587626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 309.3ns 
587627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
587627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
587628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
589951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
590713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
590904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 179.88ms 
590906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
590906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.5ns 
590907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
593216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
593981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
594030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.8ms 
594032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
594032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
594032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
596377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
597138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
597140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.9ns 
597142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
597142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
597142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
599445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
600206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
600208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 371.5ns 
600210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
600210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
600210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
602529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
603293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
603295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 384.61ns 
603296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
603296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
603297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
605597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
606358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
606360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.41ns 
606362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
606362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
606362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
608680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
609446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
609525     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
609542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.15ms 
609544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
609545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366ns 
609547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
611866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
612629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
612714     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
612716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.49ms 
612718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
612718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
612719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
615022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
615786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
615787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 
615813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
615847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
615864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
615868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
615873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
615876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
615876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
615878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
615881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
615883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
615885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
615885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
616109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
616110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
616112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
616113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
616114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
616258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
616259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
616262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
616264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
616266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
616266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
616450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
616453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
616454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
616454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
616456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
616458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
616593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
616595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
616596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
616597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
616598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
616599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
616607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
616607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
616608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
616610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
616612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
616613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
616622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
616623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
616624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
616625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
616626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
616627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
616772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
616772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
616774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
616920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
616922     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)'' 
616924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
616925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
616926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
616928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
616928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
616931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
616935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
616936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
616937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
616938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
616938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
617072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
617077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
617078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
617079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
617080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
617081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
617083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
617288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
617289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
617291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
617293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
617294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
617294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
617295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
617297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
617408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
617410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
617514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
617519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
617524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
617525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
617527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
617533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
617533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
617533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
617534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
617535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
617544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
617548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
617648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
617650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
617652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
617655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
617655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
617655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
617656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
617657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
617706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
617711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
617803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
617805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
617806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
617807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
617808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
617809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
617938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
617942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
617945     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)'' 
617946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
617947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
617948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
617949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
617950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
617958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
617963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
617965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
617965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
618064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
618065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
618066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
618067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
618068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
618068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
618174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
618175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
618176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
618178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
618178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
618179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
618179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
618180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
618261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
618263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
618363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
618364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
618364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
618371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
618375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
618380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
618505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
618506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
618506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
618507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
618518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
618605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
622130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
622131     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)'' 
622136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
622137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
622138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
622138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
622140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
622148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
622149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
622150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
622150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
622151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
622243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
622247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
622248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
622248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
622249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
622249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
622251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
622349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
622350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
622351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
622353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
622355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
622356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
622357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
622358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
622434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
622436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
622509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
622513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
622518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
622519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
622519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
622520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
622530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
622610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
622611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
622612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
622613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
622695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
622705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
622706     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)'' 
622710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
622710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
622711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
622712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
622712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
622723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
622725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
622727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
622727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
622728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
622819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
622821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
622822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
622824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
622825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
622924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
622972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
622973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
622974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
622975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
622976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
622977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
623076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
623079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
623080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
623081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
623082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
623084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
623086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
623087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
623089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
623089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
623090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
623091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
623092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
623092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
623093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
623183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
623184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
623191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
623271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
623354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
623355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
623356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
623357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
623357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
623358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
623358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
623358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
623360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
623447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
623457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
623550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
623552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
623553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
623554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
623554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
623555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
623555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
623556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
623561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
623561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
623641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
623646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
623651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
623751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
623752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
623753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
623754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
623754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
623754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
623755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
623755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
623810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
623811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
623812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
623813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
623813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
623819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
623824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
623942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
624033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
624034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
624035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
624036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
624204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
624293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
624293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
627408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
627413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
627414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
627415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
627415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
627530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
627531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
627532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
627533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
627533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
627639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
630991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
634233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
634238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
634238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
634239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
634240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
634353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
634355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
634356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
634357     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)' ...' 
634358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
635534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
635534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
635535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
637901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
638686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
638687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
638688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
638694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
638705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
638707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
638709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
638709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
638713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
638714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
638716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
638719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
638719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
638727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
638729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
638729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
638859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
638861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
638861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
638862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
638863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
638930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
638931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
638932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
638933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
638933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
638937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
638937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
638938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
638939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
638940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
638940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
639025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
639026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
639027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
639028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
639029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
639029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
639116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
639117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
639118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
639119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
639119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
639120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
639121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
639121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
639122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
639123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
639123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
639124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
639124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
639125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
639125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
639126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
639126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
639127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
639128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
639130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
639169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
639170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
639222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
639223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
639225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
639225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
639226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
639273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
639275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
639277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
639278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
639279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
639280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
639281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
639321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
639323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
639326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
639376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
639429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
639429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.4ns 
639430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
641778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
642577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
642608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.95ms