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

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

tests
0

failures
0

ignored
15m25.46s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.445s passed
powPositiveConcrete data()[101] 4.497s passed
powGeq1Concrete data()[102] 4.419s passed
pow2InIntLower data()[103] 4.469s passed
pow2InIntUpper data()[104] 4.453s passed
logSelfConcrete data()[105] 4.648s passed
log1Concrete data()[106] 4.436s passed
logProduct data()[107] 4.533s passed
logTimesBaseConcrete data()[108] 4.479s passed
logProdIdentity data()[109] 4.463s passed
moduloByteIsInByte data()[10] 4.557s passed
logProdIdentityConcrete data()[110] 4.454s passed
logPowIdentity data()[111] 4.413s passed
logPowIdentityConcrete data()[112] 4.426s passed
logPositive data()[113] 4.344s passed
logPositiveConcrete data()[114] 4.374s passed
logMono data()[115] 4.353s passed
logMonoConcrete data()[116] 4.445s passed
powLogLess data()[117] 4.426s passed
powLogMore2 data()[118] 4.430s passed
logLessThanPow data()[119] 4.487s passed
moduloCharIsInChar data()[11] 4.545s passed
logLessThanPowConcrete data()[120] 4.490s passed
logSqueeze data()[121] 4.675s passed
ifthenelse_equals data()[122] 4.553s passed
ifthenelse_equals_1 data()[123] 4.567s passed
ifthenelse_equals_2 data()[124] 4.424s passed
disjointWithSingleton1 data()[125] 4.475s passed
disjointWithSingleton2 data()[126] 4.410s passed
disjointArrayRanges data()[127] 4.562s passed
disjointArrayRangeAllFields1 data()[128] 4.454s passed
disjointArrayRangeAllFields2 data()[129] 4.469s passed
div_unique1 data()[12] 4.737s passed
seqSelfDefinition data()[130] 4.563s passed
seqOutsideValue data()[131] 4.463s passed
castedGetAny data()[132] 4.520s passed
seqGetAlphaCast data()[133] 4.601s passed
getOfSeqSingleton data()[134] 4.430s passed
getOfSeqSingletonConcrete data()[135] 4.525s passed
getOfSeqConcat data()[136] 4.507s passed
getOfSeqSub data()[137] 4.566s passed
getOfSeqReverse data()[138] 4.531s passed
lenOfSeqEmpty data()[139] 4.551s passed
div_unique2 data()[13] 4.500s passed
lenOfSeqSingleton data()[140] 4.544s passed
lenOfSeqConcat data()[141] 4.581s passed
lenOfSeqSub data()[142] 4.607s passed
lenOfSeqReverse data()[143] 4.662s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.394s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.524s passed
getOfSeqSingletonEQ data()[146] 4.498s passed
getOfSeqConcatEQ data()[147] 4.490s passed
getOfSeqSubEQ data()[148] 4.473s passed
getOfSeqReverseEQ data()[149] 4.437s passed
div_exists data()[14] 4.888s passed
lenOfSeqEmptyEQ data()[150] 4.514s passed
lenOfSeqSingletonEQ data()[151] 4.477s passed
lenOfSeqConcatEQ data()[152] 4.395s passed
lenOfSeqSubEQ data()[153] 4.549s passed
lenOfSeqReverseEQ data()[154] 4.478s passed
getOfSeqDefEQ data()[155] 4.465s passed
lenOfSeqDefEQ data()[156] 4.473s passed
seqConcatWithSeqEmpty1 data()[157] 4.450s passed
seqConcatWithSeqEmpty2 data()[158] 4.567s passed
seqReverseOfSeqEmpty data()[159] 4.685s passed
div_one data()[15] 4.566s passed
subSeqComplete data()[160] 4.644s passed
subSeqTailR data()[161] 4.688s passed
subSeqTailL data()[162] 4.523s passed
subSeqTailEQR data()[163] 4.428s passed
subSeqTailEQL data()[164] 4.542s passed
seqDef_split data()[165] 4.553s passed
seqDef_induction_upper data()[166] 4.501s passed
seqDef_induction_upper_concrete data()[167] 4.567s passed
seqDef_induction_lower data()[168] 4.609s passed
seqDef_induction_lower_concrete data()[169] 4.618s passed
jdiv_one data()[16] 4.551s passed
seqDef_split_in_three data()[170] 4.682s passed
seqDef_empty data()[171] 4.549s passed
seqDef_one_summand data()[172] 4.512s passed
seqDef_lower_equals_upper data()[173] 4.640s passed
seqDefOfSeq data()[174] 4.555s passed
seqSelfDefinitionEQ2 data()[175] 4.492s passed
indexOfSeqSingleton data()[176] 4.568s passed
indexOfSeqConcatFirst data()[177] 4.570s passed
indexOfSeqConcatSecond data()[178] 4.578s passed
indexOfSeqSub data()[179] 4.599s passed
div_zero data()[17] 4.708s passed
lenOfArray2seq data()[180] 4.559s passed
getAnyOfArray2seq data()[181] 4.687s passed
getOfArray2seq data()[182] 4.508s passed
getAnyOfNPermInv data()[183] 4.538s passed
seqNPermRange data()[184] 4.635s passed
seqPermTrans data()[185] 4.581s passed
seqPermRefl data()[186] 4.541s passed
seqPermSplit data()[187] 4.523s passed
seqNPermRight data()[188] 4.958s passed
seqPermFromSwap data()[189] 4.679s passed
divResZero1 data()[18] 4.639s passed
seqPermTransAlt0 data()[190] 4.542s passed
seqPermTransAlt1 data()[191] 4.499s passed
seqPermTransAlt2 data()[192] 4.375s passed
seqPermTransAlt3 data()[193] 4.480s passed
seqPermForall data()[194] 4.632s passed
seqPermExists data()[195] 4.610s passed
schiffl_lemma_2 data()[196] 31.345s passed
schiffl_thm_1 data()[197] 5.649s passed
eqSameSeq data()[198] 4.693s passed
divResZero2 data()[19] 4.769s passed
eqTermCut data()[1] 5.596s passed
divResOne1 data()[20] 4.510s passed
divResOne2 data()[21] 4.576s passed
div_cancel1 data()[22] 4.551s passed
div_cancel2 data()[23] 4.562s passed
divAddMultDenom data()[24] 4.496s passed
divMinus data()[25] 4.571s passed
divMinusDenom data()[26] 4.615s passed
divLeastDPos data()[27] 4.564s passed
divLeastDNeg data()[28] 4.499s passed
divGreatestDPos data()[29] 4.404s passed
equivAllRight data()[2] 5.040s passed
divGreatestDNeg data()[30] 4.383s passed
divIncreasingPos data()[31] 4.428s passed
divIncreasingNeg data()[32] 4.384s passed
jdiv_zero data()[33] 4.509s passed
jdivPulloutMinusNum data()[34] 4.496s passed
jdivPulloutMinusDenom data()[35] 4.521s passed
jdiv_uniquePosPos data()[36] 4.432s passed
jdiv_uniquePosNeg data()[37] 4.399s passed
jdiv_uniqueNegPos data()[38] 4.370s passed
jdiv_uniqueNegNeg data()[39] 4.428s passed
irrflConcrete1 data()[3] 4.777s passed
jdivMultDenom1 data()[40] 4.484s passed
jdivMultDenom2 data()[41] 4.587s passed
mod_geZero data()[42] 4.558s passed
mod_lessDenom data()[43] 4.686s passed
jmod_NumPos data()[44] 4.500s passed
jmod_NumNeg data()[45] 4.472s passed
jmod_geZero data()[46] 4.441s passed
jmodNumZero data()[47] 4.501s passed
jmod_pulloutminusNum data()[48] 4.565s passed
jmod_pulloutminusDenom data()[49] 4.391s passed
irrflConcrete2 data()[4] 4.697s passed
jmodUnique1 data()[50] 4.643s passed
jmodUnique2 data()[51] 4.635s passed
intDivRem data()[52] 4.528s passed
jmodjmod data()[53] 4.577s passed
jmodDivisible data()[54] 4.518s passed
jmodDivisibleRep data()[55] 4.495s passed
jdivAddMultDenom data()[56] 4.676s passed
jmodAltZero data()[57] 4.533s passed
jmodAddMultDenomZero data()[58] 4.373s passed
polyDiv_zero data()[59] 4.375s passed
cancel_gtPos data()[5] 4.701s passed
polyMod_ltdivDenom data()[60] 4.390s passed
bsum_empty data()[61] 4.280s passed
bsum_induction_upper data()[62] 4.360s passed
bsum_induction_lower data()[63] 4.337s passed
bsum_num_of_bounds data()[64] 4.399s passed
bsum_num_of_bounds2 data()[65] 4.486s passed
bsum_induction_upper2 data()[66] 4.529s passed
bsum_induction_upper_concrete data()[67] 4.574s passed
bsum_induction_upper_concrete_2 data()[68] 4.546s passed
bsum_induction_upper2_concrete data()[69] 4.504s passed
cancel_gtNeg data()[6] 4.665s passed
bsum_induction_lower_concrete data()[70] 4.539s passed
bsum_induction_lower2 data()[71] 4.403s passed
bsum_induction_lower2_concrete data()[72] 4.499s passed
bsum_positive data()[73] 4.563s passed
bsum_upper_bound data()[74] 4.571s passed
bsum_lower_bound data()[75] 4.572s passed
bsum_positive_lower_bound_element data()[76] 4.535s passed
bsum_sub_same_index data()[77] 4.481s passed
bsum_less_same_index data()[78] 4.489s passed
bsum_equal_except_one_index data()[79] 4.454s passed
moduloIntIsInInt data()[7] 4.686s passed
bsum_num_of_is_max data()[80] 4.448s passed
bsum_num_of_is_max2 data()[81] 4.518s passed
bsum_num_of_is_max3 data()[82] 4.543s passed
bsum_num_of_is_max4 data()[83] 4.448s passed
bsum_num_of_lt_max data()[84] 4.432s passed
bsum_num_of_lt_max2 data()[85] 4.518s passed
bsum_num_of_lt_max3 data()[86] 4.556s passed
bsum_num_of_lt_max4 data()[87] 4.508s passed
bsum_num_of_gt0 data()[88] 4.530s passed
bsum_num_of_gt0_alt data()[89] 4.456s passed
moduloLongIsInLong data()[8] 4.580s passed
bsum_add_concrete data()[90] 4.449s passed
bprod_all_positive data()[91] 4.532s passed
bprod_split data()[92] 4.596s passed
powConcrete0 data()[93] 4.637s passed
powConcrete1 data()[94] 4.513s passed
powSplitFactor data()[95] 4.425s passed
powAdd data()[96] 4.367s passed
powMono data()[97] 4.464s passed
powMonoConcrete data()[98] 4.531s passed
powMonoConcreteRight data()[99] 4.399s passed
moduloShortIsInShort data()[9] 4.600s passed

Standard output

557        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 13.11ms 
873        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
898        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)

2134       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2137       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2140       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2140       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4087       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.46s 
11460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11514      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.1ns 
11533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.9ms 
11541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
15721      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
17085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
17117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.34ms 
17133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
17134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.19ns 
17136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 
20961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
22152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
22170      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.08ms 
22174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
22174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.79ns 
22177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
25776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26947      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
26952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.39ns 
26954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
30463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms 
31649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31649      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
31655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
35147      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
36259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
36347      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.48ms 
36355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
36356      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.26ms 
36358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39852      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
39853      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
41017      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.77ms 
41022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
41022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.19ns 
41024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
44587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
45701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
45706      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.39ns 
45709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
45709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.89ns 
45710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
49177      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
50282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
50286      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.09ns 
50289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
50290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 506.99ns 
50291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
53764      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
54881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
54886      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 831.79ns 
54889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
54890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 726.49ns 
54892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
58322      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
59439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
59443      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.49ns 
59447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
59447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.5ns 
59449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
62893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
63984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
63989      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
63993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
63993      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 551.19ns 
63995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
67499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
68628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
68727      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94ms 
68729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
68730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 
68731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
72104      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
73173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
73226      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.7ms 
73233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
73233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 651.49ns 
73235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
76643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
77736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
78115      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.17ms 
78120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
78120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.2ns 
78121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
81548      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
82672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
82683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
82686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
82686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.4ns 
82690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86076      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
86077      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
87231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
87235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
87238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
87239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms 
87241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90743      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
90744      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
91870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
91943      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.11ms 
91947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
91947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.39ns 
91949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95473      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
95473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
96555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
96583      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
96586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
96587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 
96589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
100181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
101326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
101353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.05ms 
101355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
101356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.5ns 
101357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
104753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
105837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
105863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.13ms 
105865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
105866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 
105867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
109311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
110414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
110439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.61ms 
110442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
110442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.3ns 
110443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
113841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
114947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
114989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.36ms 
114992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
114993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.1ns 
114995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
118434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
119548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
119552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
119554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
119555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
119556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
122883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
123981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
124048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.61ms 
124050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
124050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.8ns 
124052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
127457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
128523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
128618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.98ms 
128622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
128623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.04ms 
128626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
132036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
133159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
133235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.66ms 
133237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
133237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
133239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
136646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
137786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
137798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
137801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
137802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.59ns 
137804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
141194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
142265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
142298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.9ms 
142300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
142301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
142304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
145622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
146681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
146702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.77ms 
146704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
146704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.7ns 
146705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
150058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
151072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
151084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
151087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
151087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349ns 
151089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
154420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
155496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
155511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.12ms 
155517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
155517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.89ns 
155518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
158829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
159888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
159898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
159900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
159900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
159901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
163308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
164402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
164407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
164409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
164409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
164410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
167816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
168880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
168902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.88ms 
168911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
168912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 527.29ns 
168913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
172215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
173339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
173424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.34ms 
173427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
173428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.1ns 
173429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
176755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
177828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
177857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24ms 
177859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
177859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.8ns 
177860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
181161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
182229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
182256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.7ms 
182258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
182258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
182259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
185505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
186595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
186626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.96ms 
186627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
186628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
186629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
189979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
191028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
191054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.95ms 
191056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
191056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.9ns 
191057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
194372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
195472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
195537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.34ms 
195539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
195540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.2ns 
195541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
198980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
200120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
200124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
200127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
200127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.1ns 
200128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
203639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
204676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
204683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
204685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
204686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.2ns 
204687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
208233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
209358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
209370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
209371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
209371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
209372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
212772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
213856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
213869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ms 
213870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
213871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
213872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
217213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
218313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
218341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.95ms 
218343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
218343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.5ns 
218344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
221681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
222769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
222781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
222784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
222785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.1ns 
222786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
226182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
227277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
227282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
227285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
227286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.3ns 
227288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
230767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
231842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
231848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
231851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
231851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310ns 
231852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
235178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
236234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
236240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
236242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
236242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
236243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
239613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
240702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
240882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 166.47ms 
240891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
240891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.89ns 
240893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
244280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
245390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
245523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.61ms 
245526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
245526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.5ns 
245528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
248955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
250045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
250051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
250054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
250054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 
250056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
253467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
254571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
254629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.84ms 
254631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
254631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237ns 
254633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
258023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
259104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
259146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.33ms 
259148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
259149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
259149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
262540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
263635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
263641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
263649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
263649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.3ns 
263651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
267001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
268093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
268322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 210.28ms 
268326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
268327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.8ns 
268328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
271724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
272840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
272857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
272858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
272859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
272859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
276170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
277218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
277231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
277232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
277233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
277234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
280515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
281576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
281605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.29ms 
281607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
281607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
281608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
284919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
285974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
285994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
285997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
285997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
285998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
289249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
290270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
290275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
290278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
290278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.5ns 
290279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
293565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
294627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
294635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
294639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
294639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
294640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
297878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
298933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
298969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.71ms 
298977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
298977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314ns 
298979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
302284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
303346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
303374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.34ms 
303376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
303376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
303377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
306705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
307828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
307860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.01ms 
307862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
307862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
307863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
311275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
312385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
312390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
312391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
312391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
312393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
315838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
316956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
316963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
316965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
316965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
316966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
320433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
321502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
321509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
321511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
321511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
321512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
324921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
326009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
326013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
326015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
326015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
326016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
329434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
330549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
330552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.69ns 
330555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
330555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
330556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
333880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
334950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
334955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
334957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
334957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns 
334958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
338370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
339448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
339452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
339455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
339456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
339457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
342855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
343937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
344016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.44ms 
344019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
344020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.4ns 
344021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
347437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
348524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
348588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.72ms 
348590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
348590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
348591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
351991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
353090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
353160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.05ms 
353165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
353166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 762.2ns 
353167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
356571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
357611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
357695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.38ms 
357698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
357698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
357727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
361034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
362101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
362177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.53ms 
362179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
362179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
362180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
365484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
366582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
366666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.71ms 
366668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
366668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
366670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
370018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
371078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
371120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.49ms 
371122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
371122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
371123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
374450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
375539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
375568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
375569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
375570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
375570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
378908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
380039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
380086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.41ms 
380087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
380088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.6ns 
380089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
383503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
384601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
384629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.85ms 
384631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
384631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
384632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
387994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
389031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
389077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.79ms 
389080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
389080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
389081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
392407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
393472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
393509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.22ms 
393511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
393511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
393512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
396894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
397986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
398027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.35ms 
398029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
398029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
398030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
401460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
402546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
402583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.35ms 
402585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
402585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.3ns 
402586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
405969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
407053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
407091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.55ms 
407093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
407093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
407094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
410512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
411582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
411621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.78ms 
411623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
411623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
411624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
414956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
416039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
416077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.35ms 
416078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
416079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
416079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
419429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
420512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
420526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
420527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
420527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
420528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
423880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
425027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
425058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.43ms 
425060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
425060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
425061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
428491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
429649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
429655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
429656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
429656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
429657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
433164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
434287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
434291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830.9ns 
434294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
434294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.8ns 
434295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
437720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
438801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
438804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.1ns 
438805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
438806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
438806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
442167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
443219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
443229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.06ms 
443231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
443231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
443232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
446533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
447586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
447596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
447597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
447597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
447598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
450964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
452037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
452060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.05ms 
452061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
452061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
452063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
455511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
456586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
456591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
456593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
456593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
456594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
459897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
460988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
460991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.89ns 
460992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
460992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
460993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
464380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
465427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
465435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 
465437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
465437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
465438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
468845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
469929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
469932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.7ns 
469934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
469934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
469935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
473260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
474348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
474351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.2ns 
474353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
474353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
474354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
477720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
478817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
478820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.7ns 
478822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
478822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
478823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
482148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
483267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
483273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
483275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
483275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
483276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
486819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
487909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
487922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ms 
487923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
487923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
487924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
491260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
492352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
492357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
492359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
492359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
492360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
495837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
496879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
496890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
496892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
496892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
496893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
500316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
501360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
501367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
501372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
501372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.7ns 
501373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
504734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
505811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
505833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.99ms 
505835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
505835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
505836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
509175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
510282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
510287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
510289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
510289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
510290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
513649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
514696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
514700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
514702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
514702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
514703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
518052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
519120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
519126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
519127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
519127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
519128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
522401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
523443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
523470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.01ms 
523472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
523472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.8ns 
523473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
526757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
527836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
527843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931ns 
527846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
527846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
527847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
531125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
532137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
532197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.44ms 
532199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
532199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
532199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
535581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
536637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
536642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
536644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
536644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
536644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
539954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
541036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
541068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.34ms 
541070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
541070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
541071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
544342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
545462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
545498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.15ms 
545500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
545500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
545501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
548889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
549942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
549985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.39ms 
549987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
549987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
549988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
553397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
554471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
554475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.1ns 
554477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
554477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
554477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
558025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
559143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
559151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
559152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
559152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
559153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
562597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
563699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
563704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
563705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
563705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
563706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
567190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
568266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
568270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
568272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
568272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
568273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
571605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
572691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
572694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
572696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
572696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
572697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
576066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
577163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
577169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
577171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
577171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
577172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
580507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
581574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
581579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
581581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
581581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
581582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
585035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
586126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
586141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.23ms 
586142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
586142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
586143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
589504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
590571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
590588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.69ms 
590600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
590600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.6ns 
590602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
593952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
595041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
595065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
595068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
595069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.6ns 
595070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
598451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
599595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
599629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.83ms 
599631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
599631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.3ns 
599632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
602983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
604084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
604091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
604094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
604094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 
604095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
607475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
608597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
608612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
608614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
608614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
608615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
612106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
613205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
613213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
613215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
613215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
613215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
616549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
617638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
617643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
617645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
617645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.4ns 
617646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
621045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
622165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
622168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
622170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
622170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.6ns 
622171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
625539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
626658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
626675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.73ms 
626678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
626678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
626679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
630139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
631236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
631242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
631244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
631244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
631245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
634635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
635762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
635773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
635775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
635775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
635776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
639166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
640321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
640325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
640326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
640326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
640327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
643731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
644865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
644869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.4ns 
644870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
644870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
644871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
648332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
649442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
649449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
649451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
649451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
649452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
652944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
654052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
654056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
654058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
654058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
654058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
657551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
658681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
658718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
658719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
658719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
658720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
662025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
663109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
663113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
663114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
663114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
663115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
666448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
667628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
667637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
667638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
667638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
667639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
671039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
672129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
672134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
672136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
672136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.5ns 
672137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
675507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
676607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
676624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
676626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
676626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
676626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
680000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
681095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
681098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.9ns 
681099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
681099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
681100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
684422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
685521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
685534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
685536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
685536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
685537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
688962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
690040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
690047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
690050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
690050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
690051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
693420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
694523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
694526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
694527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
694527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
694528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
697834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
698914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
698920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
698922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
698922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
698923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
702331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
703465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
703470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
703471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
703471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
703472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
706847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
707943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
707948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
707949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
707949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
707950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
711315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
712407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
712412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
712414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
712414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
712414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
715783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
716878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
716886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
716887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
716887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
716888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
720229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
721315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
721335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ms 
721337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
721337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
721338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
724753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
725880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
725902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.92ms 
725904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
725904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 
725905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
729436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
730570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
730586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
730589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
730589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
730590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
734090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
735215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
735231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 
735233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
735233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
735234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
738739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
739877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
739919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.38ms 
739921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
739921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
739922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
743301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
744406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
744442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.92ms 
744444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
744444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
744445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
747752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
748836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
748870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.38ms 
748872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
748872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
748873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
752286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
753390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
753412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
753414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
753414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
753415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
756781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
757882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
757965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.51ms 
757966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
757966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
757967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
761293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
762384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
762466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.21ms 
762468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
762468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
762470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
765823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
766966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
767033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.51ms 
767035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
767035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
767036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
770443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
771573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
771642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.55ms 
771644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
771644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
771645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
775088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
776190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
776258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.48ms 
776262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
776262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
776263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
779646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
780759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
780942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 173.02ms 
780944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
780944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
780945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
784370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
785478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
785491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
785493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
785493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
785494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
788888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
789993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
790003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.32ms 
790005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
790005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
790006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
793451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
794635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
794643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
794646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
794646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
794646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
798030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
799172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
799198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.85ms 
799200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
799200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
799201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
802529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
803671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
803690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
803692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
803692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
803693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
807150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
808254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
808259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
808260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
808260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
808261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
811701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
812804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
812828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.92ms 
812830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
812830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
812831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
816304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
817380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
817407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.46ms 
817408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
817408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116ns 
817409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
820837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
821974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
822005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.55ms 
822007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
822007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
822007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
825457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
826560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
826564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
826566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
826566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
826567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
830094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
831245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
831251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
831253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
831253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
831254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
834660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
835749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
835759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
835761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
835761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
835762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
839186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
840287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
840297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
840299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
840299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
840300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
843685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
843685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
844806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
844932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.68ms 
844935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
844935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
844936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
848317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
849459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
849512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.47ms 
849515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
849515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
849516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
852906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
852906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
854017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
854054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.31ms 
854056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
854056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
854057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
857471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
857471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
858574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
858577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 396.4ns 
858580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
858580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
858581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
862099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
863241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
863536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.23ms 
863538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
863538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
863539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
866983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
866984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
868122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
868214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.78ms 
868218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
868218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.2ns 
868219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
871614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
871614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
872754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
872757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.3ns 
872759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
872759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
872760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
876164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
876164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
877254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
877256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.9ns 
877258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
877258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
877259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
880546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
880546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
881628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
881631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.1ns 
881632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
881632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
881633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
884989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
886109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
886111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.5ns 
886113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
886113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
886114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
889494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
889495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
890594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
890742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 145.39ms 
890746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
890746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.7ns 
890747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
894174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
895265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
895353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.94ms 
895355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
895355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
895357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
898863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
898864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
899994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
899996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
900033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
900125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
900154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
900166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
900178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
900183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
900185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
900189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
900197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
900202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
900209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
900213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
900545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
900548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
900549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
900553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
900556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
900751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
900753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
900755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
900757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
900758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
900759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
901036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
901039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
901040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
901041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
901042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
901044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
901233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
901235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
901236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
901238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
901239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
901240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
901251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
901253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
901254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
901256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
901258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
901259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
901268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
901270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
901271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
901272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
901273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
901275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
901497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
901499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
901500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
901669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
901671     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)'' 
901674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
901675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
901677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
901677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
901679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
901680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
901687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
901689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
901691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
901692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
901693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
901851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
901857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
901859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
901860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
901861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
901862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
901863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
902015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
902017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
902018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
902020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
902021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
902022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
902022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
902024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
902132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
902134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
902261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
902267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
902273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
902274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
902275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
902277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
902277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
902278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
902278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
902280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
902293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
902300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
902418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
902420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
902421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
902423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
902424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
902424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
902425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
902432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
902496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
902503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
902621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
902624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
902626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
902628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
902629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
902630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
902816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
902821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
902822     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)'' 
902824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
902825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
902827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
902827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
902828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
902840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
902842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
902843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
902844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
902978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
902980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
902980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
902981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
902983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
902984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
903135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
903137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
903139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
903141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
903142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
903143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
903143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
903146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
903263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
903267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
903378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
903379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
903381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
903387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
903393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
903398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
903584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
903586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
903587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
903588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
903603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
903732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
908648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
908650     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)'' 
908659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
908660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
908661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
908662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
908662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
908673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
908675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
908676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
908677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
908678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
908810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
908814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
908816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
908816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
908817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
908818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
908819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
908954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
908955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
908956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
908957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
908958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
908959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
908959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
908960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
909063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
909065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
909169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
909175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
909180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
909181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
909182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
909183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
909197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
909316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
909317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
909318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
909319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
909424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
909437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
909438     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)'' 
909445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
909446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
909447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
909448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
909449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
909467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
909470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
909471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
909472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
909473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
909599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
909601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
909603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
909605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
909606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
909793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
909798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
909799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
909800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
909801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
909801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
909802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
909935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
909937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
909938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
909939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
909940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
909940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
909941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
909942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
909943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
909944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
909946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
909947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
909948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
909948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
909949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
910073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
910075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
910083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
910189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
910304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
910305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
910306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
910307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
910308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
910308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
910309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
910309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
910310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
910427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
910435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
910559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
910567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
910568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
910569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
910570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
910570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
910571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
910572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
910579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
910580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
910693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
910700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
910707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
910842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
910843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
910844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
910845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
910846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
910846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
910846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
910847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
910920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
910921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
910922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
910923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
910924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
910931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
910939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
911105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
911239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
911241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
911241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
911243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
911472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
911590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
911591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
915851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
915860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
915861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
915863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
915864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
916024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
916025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
916027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
916027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
916028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
916174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
920378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
924929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
924934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
924935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
924936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
924937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
925089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
925090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
925091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
925095     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)' ...' 
925096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
926699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
926699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
926701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
930167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
930168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
931270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
931273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
931274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
931302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
931316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
931319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
931321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
931322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
931331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
931333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
931338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
931342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
931343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
931357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
931359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
931360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
931424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
931426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
931426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
931427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
931429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
931525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
931526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
931530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
931531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
931532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
931539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
931540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
931540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
931542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
931543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
931544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
931657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
931658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
931659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
931661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
931662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
931662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
931791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
931793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
931793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
931794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
931795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
931796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
931797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
931798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
931799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
931799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
931800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
931801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
931801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
931802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
931804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
931805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
931813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
931819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
931820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
931824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
931895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
931897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
932047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
932049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
932051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
932052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
932053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
932054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
932120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
932123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
932125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
932127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
932128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
932129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
932130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
932191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
932194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
932197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
932271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
932350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
932351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589ns 
932352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
935795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
935795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
936990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
937039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.61ms