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

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

tests
0

failures
0

ignored
11m30.53s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.388s passed
powPositiveConcrete data()[101] 3.347s passed
powGeq1Concrete data()[102] 3.347s passed
pow2InIntLower data()[103] 3.387s passed
pow2InIntUpper data()[104] 3.343s passed
logSelfConcrete data()[105] 3.350s passed
log1Concrete data()[106] 3.362s passed
logProduct data()[107] 3.338s passed
logTimesBaseConcrete data()[108] 3.343s passed
logProdIdentity data()[109] 3.364s passed
moduloByteIsInByte data()[10] 3.425s passed
logProdIdentityConcrete data()[110] 3.380s passed
logPowIdentity data()[111] 3.348s passed
logPowIdentityConcrete data()[112] 3.354s passed
logPositive data()[113] 3.372s passed
logPositiveConcrete data()[114] 3.353s passed
logMono data()[115] 3.368s passed
logMonoConcrete data()[116] 3.335s passed
powLogLess data()[117] 3.353s passed
powLogMore2 data()[118] 3.378s passed
logLessThanPow data()[119] 3.399s passed
moduloCharIsInChar data()[11] 3.416s passed
logLessThanPowConcrete data()[120] 3.353s passed
logSqueeze data()[121] 3.352s passed
ifthenelse_equals data()[122] 3.341s passed
ifthenelse_equals_1 data()[123] 3.336s passed
ifthenelse_equals_2 data()[124] 3.340s passed
disjointWithSingleton1 data()[125] 3.336s passed
disjointWithSingleton2 data()[126] 3.339s passed
disjointArrayRanges data()[127] 3.374s passed
disjointArrayRangeAllFields1 data()[128] 3.354s passed
disjointArrayRangeAllFields2 data()[129] 3.370s passed
div_unique1 data()[12] 3.523s passed
seqSelfDefinition data()[130] 3.377s passed
seqOutsideValue data()[131] 3.362s passed
castedGetAny data()[132] 3.385s passed
seqGetAlphaCast data()[133] 3.365s passed
getOfSeqSingleton data()[134] 3.356s passed
getOfSeqSingletonConcrete data()[135] 3.352s passed
getOfSeqConcat data()[136] 3.374s passed
getOfSeqSub data()[137] 3.378s passed
getOfSeqReverse data()[138] 3.348s passed
lenOfSeqEmpty data()[139] 3.359s passed
div_unique2 data()[13] 3.442s passed
lenOfSeqSingleton data()[140] 3.376s passed
lenOfSeqConcat data()[141] 3.363s passed
lenOfSeqSub data()[142] 3.356s passed
lenOfSeqReverse data()[143] 3.353s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.375s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.359s passed
getOfSeqSingletonEQ data()[146] 3.351s passed
getOfSeqConcatEQ data()[147] 3.450s passed
getOfSeqSubEQ data()[148] 3.353s passed
getOfSeqReverseEQ data()[149] 3.375s passed
div_exists data()[14] 3.590s passed
lenOfSeqEmptyEQ data()[150] 3.355s passed
lenOfSeqSingletonEQ data()[151] 3.348s passed
lenOfSeqConcatEQ data()[152] 3.376s passed
lenOfSeqSubEQ data()[153] 3.355s passed
lenOfSeqReverseEQ data()[154] 3.372s passed
getOfSeqDefEQ data()[155] 3.354s passed
lenOfSeqDefEQ data()[156] 3.354s passed
seqConcatWithSeqEmpty1 data()[157] 3.385s passed
seqConcatWithSeqEmpty2 data()[158] 3.361s passed
seqReverseOfSeqEmpty data()[159] 3.382s passed
div_one data()[15] 3.400s passed
subSeqComplete data()[160] 3.364s passed
subSeqTailR data()[161] 3.396s passed
subSeqTailL data()[162] 3.365s passed
subSeqTailEQR data()[163] 3.394s passed
subSeqTailEQL data()[164] 3.362s passed
seqDef_split data()[165] 3.400s passed
seqDef_induction_upper data()[166] 3.415s passed
seqDef_induction_upper_concrete data()[167] 3.387s passed
seqDef_induction_lower data()[168] 3.409s passed
seqDef_induction_lower_concrete data()[169] 3.392s passed
jdiv_one data()[16] 3.378s passed
seqDef_split_in_three data()[170] 3.476s passed
seqDef_empty data()[171] 3.384s passed
seqDef_one_summand data()[172] 3.360s passed
seqDef_lower_equals_upper data()[173] 3.369s passed
seqDefOfSeq data()[174] 3.414s passed
seqSelfDefinitionEQ2 data()[175] 3.378s passed
indexOfSeqSingleton data()[176] 3.382s passed
indexOfSeqConcatFirst data()[177] 3.390s passed
indexOfSeqConcatSecond data()[178] 3.377s passed
indexOfSeqSub data()[179] 3.394s passed
div_zero data()[17] 3.444s passed
lenOfArray2seq data()[180] 3.377s passed
getAnyOfArray2seq data()[181] 3.359s passed
getOfArray2seq data()[182] 3.374s passed
getAnyOfNPermInv data()[183] 3.377s passed
seqNPermRange data()[184] 3.460s passed
seqPermTrans data()[185] 3.446s passed
seqPermRefl data()[186] 3.393s passed
seqPermSplit data()[187] 3.379s passed
seqNPermRight data()[188] 3.562s passed
seqPermFromSwap data()[189] 3.434s passed
divResZero1 data()[18] 3.419s passed
seqPermTransAlt0 data()[190] 3.365s passed
seqPermTransAlt1 data()[191] 3.360s passed
seqPermTransAlt2 data()[192] 3.373s passed
seqPermTransAlt3 data()[193] 3.348s passed
seqPermForall data()[194] 3.462s passed
seqPermExists data()[195] 3.449s passed
schiffl_lemma_2 data()[196] 21.892s passed
schiffl_thm_1 data()[197] 4.208s passed
eqSameSeq data()[198] 3.476s passed
divResZero2 data()[19] 3.406s passed
eqTermCut data()[1] 3.946s passed
divResOne1 data()[20] 3.445s passed
divResOne2 data()[21] 3.407s passed
div_cancel1 data()[22] 3.379s passed
div_cancel2 data()[23] 3.371s passed
divAddMultDenom data()[24] 3.448s passed
divMinus data()[25] 3.456s passed
divMinusDenom data()[26] 3.406s passed
divLeastDPos data()[27] 3.394s passed
divLeastDNeg data()[28] 3.366s passed
divGreatestDPos data()[29] 3.381s passed
equivAllRight data()[2] 3.801s passed
divGreatestDNeg data()[30] 3.365s passed
divIncreasingPos data()[31] 3.360s passed
divIncreasingNeg data()[32] 3.358s passed
jdiv_zero data()[33] 3.363s passed
jdivPulloutMinusNum data()[34] 3.359s passed
jdivPulloutMinusDenom data()[35] 3.399s passed
jdiv_uniquePosPos data()[36] 3.367s passed
jdiv_uniquePosNeg data()[37] 3.387s passed
jdiv_uniqueNegPos data()[38] 3.369s passed
jdiv_uniqueNegNeg data()[39] 3.375s passed
irrflConcrete1 data()[3] 3.774s passed
jdivMultDenom1 data()[40] 3.388s passed
jdivMultDenom2 data()[41] 3.354s passed
mod_geZero data()[42] 3.380s passed
mod_lessDenom data()[43] 3.383s passed
jmod_NumPos data()[44] 3.355s passed
jmod_NumNeg data()[45] 3.370s passed
jmod_geZero data()[46] 3.380s passed
jmodNumZero data()[47] 3.357s passed
jmod_pulloutminusNum data()[48] 3.363s passed
jmod_pulloutminusDenom data()[49] 3.359s passed
irrflConcrete2 data()[4] 3.606s passed
jmodUnique1 data()[50] 3.420s passed
jmodUnique2 data()[51] 3.423s passed
intDivRem data()[52] 3.344s passed
jmodjmod data()[53] 3.367s passed
jmodDivisible data()[54] 3.360s passed
jmodDivisibleRep data()[55] 3.360s passed
jdivAddMultDenom data()[56] 3.487s passed
jmodAltZero data()[57] 3.358s passed
jmodAddMultDenomZero data()[58] 3.358s passed
polyDiv_zero data()[59] 3.348s passed
cancel_gtPos data()[5] 3.524s passed
polyMod_ltdivDenom data()[60] 3.351s passed
bsum_empty data()[61] 3.335s passed
bsum_induction_upper data()[62] 3.333s passed
bsum_induction_lower data()[63] 3.351s passed
bsum_num_of_bounds data()[64] 3.387s passed
bsum_num_of_bounds2 data()[65] 3.399s passed
bsum_induction_upper2 data()[66] 3.350s passed
bsum_induction_upper_concrete data()[67] 3.349s passed
bsum_induction_upper_concrete_2 data()[68] 3.343s passed
bsum_induction_upper2_concrete data()[69] 3.345s passed
cancel_gtNeg data()[6] 3.514s passed
bsum_induction_lower_concrete data()[70] 3.340s passed
bsum_induction_lower2 data()[71] 3.333s passed
bsum_induction_lower2_concrete data()[72] 3.332s passed
bsum_positive data()[73] 3.413s passed
bsum_upper_bound data()[74] 3.400s passed
bsum_lower_bound data()[75] 3.377s passed
bsum_positive_lower_bound_element data()[76] 3.418s passed
bsum_sub_same_index data()[77] 3.382s passed
bsum_less_same_index data()[78] 3.383s passed
bsum_equal_except_one_index data()[79] 3.423s passed
moduloIntIsInInt data()[7] 3.473s passed
bsum_num_of_is_max data()[80] 3.367s passed
bsum_num_of_is_max2 data()[81] 3.369s passed
bsum_num_of_is_max3 data()[82] 3.412s passed
bsum_num_of_is_max4 data()[83] 3.365s passed
bsum_num_of_lt_max data()[84] 3.363s passed
bsum_num_of_lt_max2 data()[85] 3.375s passed
bsum_num_of_lt_max3 data()[86] 3.382s passed
bsum_num_of_lt_max4 data()[87] 3.378s passed
bsum_num_of_gt0 data()[88] 3.363s passed
bsum_num_of_gt0_alt data()[89] 3.352s passed
moduloLongIsInLong data()[8] 3.466s passed
bsum_add_concrete data()[90] 3.339s passed
bprod_all_positive data()[91] 3.383s passed
bprod_split data()[92] 3.350s passed
powConcrete0 data()[93] 3.350s passed
powConcrete1 data()[94] 3.368s passed
powSplitFactor data()[95] 3.363s passed
powAdd data()[96] 3.360s passed
powMono data()[97] 3.368s passed
powMonoConcrete data()[98] 3.357s passed
powMonoConcreteRight data()[99] 3.348s passed
moduloShortIsInShort data()[9] 3.439s passed

Standard output

366        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
388        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.13ms 
617        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635        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)

1752       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1753       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1757       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1757       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3202       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8993       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.38s 
9059       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9095       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.8ns 
9111       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9111       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544ns 
9116       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12082      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
12084      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms 
13056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13056      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.6ns 
13058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
15925      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16855      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.58ms 
16858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.5ns 
16859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
19667      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20627      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms 
20632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns 
20633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
23316      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
24220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24234      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.31ms 
24238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 836.31ns 
24241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
26862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.39ms 
27761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 
27762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30403      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
30404      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31273      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.22ms 
31279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.8ns 
31281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
33915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34751      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847.31ns 
34753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.3ns 
34755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
37369      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
38217      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.11ns 
38219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
38219      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
38220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
40806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41655      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.9ns 
41658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.7ns 
41660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44222      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
44223      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
45078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
45081      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.21ns 
45083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
45084      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.3ns 
45085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
47652      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48497      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.5ns 
48500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.5ns 
48502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
51071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
52020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.55ms 
52026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
52030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.58ms 
52031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
54592      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55467      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.49ms 
55469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55469      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
55470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
58018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
59055      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.79ms 
59058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
59060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.58ms 
59061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
61613      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62456      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
62458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.5ns 
62459      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
65021      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
65837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65837      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.1ns 
65838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
68410      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
69237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69278      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.32ms 
69283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.3ns 
69284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71853      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
71854      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72699      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
72701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
72702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75248      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
75249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
76090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
76105      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
76106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
76107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
76112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78688      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
78688      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.48ms 
79552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324ns 
79554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
82109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
82958      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns 
82960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
85485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86337      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.48ms 
86338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
86339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
88874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89707      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
89709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
89710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
92249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
93108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
93155      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.88ms 
93158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
93158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.8ns 
93159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
95749      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.92ms 
96613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96613      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334ns 
96614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
99169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
100017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.85ms 
100019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
100019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
100020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
102575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
103413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.1ns 
103414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
105938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
106778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
106779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
109316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.83ms 
110159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.8ns 
110160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
112687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
113524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
113525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
116045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
116885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
116886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
119403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
120242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
120243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
122773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
123605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
123606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
126150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
126953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
126963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
126964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
126964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
126965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
129514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.42ms 
130364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
130365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
132908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
133712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
133729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
133730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
133730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
133731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
136273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
137118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
137119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
139644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
140487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
140488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
143018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
143844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
143860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
143861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
143861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
143862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
146385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.17ms 
147251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.8ns 
147252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
149774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
150599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
150602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.11ns 
150604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
150604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.9ns 
150605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
153120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
153969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
153982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
153984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
153985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 876.51ns 
153986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
156523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
157367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.4ns 
157368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
159907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
160712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
160720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
160722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
160723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.5ns 
160724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
163271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
164092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
164093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
166634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
167463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
167470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
167471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
167471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
167472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
169996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
170824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
170827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
170829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
170830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.5ns 
170830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
173362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
174187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
174190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
174191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
174192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
174192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
176714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
177542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
177549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
177552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
177553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 745.21ns 
177554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
180078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
180904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
180971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.02ms 
180972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
180972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
180973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
183494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
184393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.9ms 
184396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
184396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.2ns 
184397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
186933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
187734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
187737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
187739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
187740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.8ns 
187740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
190271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
191070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
191103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.24ms 
191106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
191106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.8ns 
191107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
193637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
194438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
194465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.65ms 
194466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
194466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
194467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
196996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
197822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
197825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
197830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
197830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
197831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
200351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
201174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
201310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 124.73ms 
201313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
201313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.9ns 
201314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
203834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
204660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
204670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
204671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
204671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
204672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
207189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
208013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
208027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms 
208029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
208029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.8ns 
208031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
210537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
211360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
211375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
211377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
211377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
211377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
213890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
214714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
214725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
214727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
214727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
214728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
217252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
218055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
218061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
218063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
218063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
218064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
220590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
221390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
221394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
221396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
221396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
221396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
223925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
224725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
224745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.66ms 
224746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
224746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
224747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
227291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
228117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
228132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
228133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
228134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
228134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
230676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
231516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
231531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms 
231533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
231534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 
231535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
234053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
234876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
234880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
234885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
234886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns 
234886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
237403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
238226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
238230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
238231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
238232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
238232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
240743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
241568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
241574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
241575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
241575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
241576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
244093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
244915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
244918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
244920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
244920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
244920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
247434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
248256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
248258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.9ns 
248259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
248260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
248260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
250788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
251588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
251592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
251593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
251593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
251594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
254120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
254921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
254924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.81ns 
254925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
254925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
254926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
257487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
258288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
258335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.38ms 
258338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
258338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.4ns 
258363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
260875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
261697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
261736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.75ms 
261738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
261738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
261739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
264249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
265072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
265113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.57ms 
265116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
265116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.4ns 
265117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
267650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
268478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
268530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.02ms 
268533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
268533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.2ns 
268534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
271057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
271882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
271914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.78ms 
271915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
271915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
271916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
274425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
275248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
275297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.98ms 
275298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
275298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
275299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
277867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
278693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
278719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.31ms 
278720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
278721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
278721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
281265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
282067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
282086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.08ms 
282087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
282088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
282088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
284630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
285432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
285455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
285457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
285457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
285457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
288025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
288849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
288867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
288868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
288868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
288869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
291385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
292207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
292232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
292234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
292234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
292234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
294749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
295573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
295596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.83ms 
295597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
295597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
295598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
298116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
298947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
298970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
298972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
298972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
298973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
301498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
302326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
302350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.36ms 
302354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
302355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 639.2ns 
302355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
304888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
305711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
305730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
305732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
305732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
305732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
308269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
309072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
309094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.79ms 
309095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
309095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
309096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
311624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
312423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
312445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.46ms 
312446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
312446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
312447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
314979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
315777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
315784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
315785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
315785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
315786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
318322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
319150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
319167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ms 
319170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
319170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns 
319171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
321691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
322515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
322519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
322520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
322520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
322520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
325037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
325865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
325868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.41ns 
325869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
325869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
325870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
328402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
329234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
329236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.11ns 
329238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
329238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.9ns 
329239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
331766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
332591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
332599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
332601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
332601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
332602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
335126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
335953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
335959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
335961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
335961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
335961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
338485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
339315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
339327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
339329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
339329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 
339330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
341877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
342681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
342684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
342686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
342686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
342686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
345227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
346031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
346033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.6ns 
346034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
346034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
346035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
348582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
349387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
349420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.11ms 
349421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
349421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
349422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
351938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
352766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
352768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.71ns 
352769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
352769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
352770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
355286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
356113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
356115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.5ns 
356116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
356116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
356117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
358671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
359498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
359501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.5ns 
359503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
359503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237ns 
359504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
362017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
362841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
362844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
362845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
362845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
362846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
365362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
366185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
366194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
366195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
366196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
366196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
368718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
369553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
369557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
369558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
369558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
369559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
372086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
372887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
372894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
372895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
372895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
372896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
375430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
376233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
376238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
376239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
376239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
376239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
378782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
379586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
379601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.47ms 
379603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
379603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
379603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
382145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
382978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
382981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
382982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
382982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
382983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
385498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
386327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
386330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
386331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
386331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
386331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
388849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
389680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
389683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
389685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
389685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
389685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
392210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
393039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
393055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
393056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
393056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
393057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
395578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
396404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
396408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 477ns 
396410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
396410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
396411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
398920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
399740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
399776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.84ms 
399778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
399778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
399778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
402283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
403108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
403111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
403112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
403112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
403113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
405644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
406444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
406465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.38ms 
406466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
406466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
406467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
409015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
409820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
409842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.58ms 
409843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
409844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
409844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
412385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
413219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
413241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.65ms 
413243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
413243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
413244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
415765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
416592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
416595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.7ns 
416596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
416596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
416596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
419114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
419941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
419946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
419947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
419947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
419948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
422457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
423284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
423287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
423288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
423288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
423289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
425794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
426621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
426624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.71ns 
426625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
426625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
426626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
429133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
429961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
429963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.51ns 
429964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
429964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
429965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
432490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
433296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
433300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
433301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
433301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
433301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
435828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
436636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
436639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
436640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
436640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
436641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
439172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
440003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
440012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ms 
440014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
440014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
440014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
442525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
443355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
443366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms 
443367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
443368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
443368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
445883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
446722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
446736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
446738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
446738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
446739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
449262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
450102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
450114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.69ms 
450115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
450115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
450116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
452654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
453471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
453475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
453477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
453477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
453477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
456016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
456855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
456861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
456862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
456862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
456863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
459380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
460220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
460223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 899.01ns 
460227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
460227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.2ns 
460228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
462740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
463578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
463581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
463582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
463582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
463583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
466094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
466930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
466933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.51ns 
466934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
466934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
466935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
469479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
470296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
470307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
470308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
470308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
470309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
472842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
473681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
473685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
473686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
473687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
473687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
476189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
477026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
477033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
477034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
477034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
477035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
479575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
480390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
480392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.41ns 
480393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
480394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
480394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
482929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
483767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
483769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.8ns 
483770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
483770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
483771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
486289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
487128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
487131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
487132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
487132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
487133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
489646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
490485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
490487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
490489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
490489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
490489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
493021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
493838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
493841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
493842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
493842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
493843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
496375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
497212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
497215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
497216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
497216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
497217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
499731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
500569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
500574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
500576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
500576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
500576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
503106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
503922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
503925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
503926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
503926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
503927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
506494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
507365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
507375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.24ms 
507376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
507377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
507377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
509889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
510726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
510728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610ns 
510729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
510729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
510730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
513261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
514097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
514103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
514104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
514104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
514105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
516619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
517456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
517458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.01ns 
517459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
517459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
517460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
519988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
520804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
520806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.81ns 
520808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
520808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
520808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
523338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
524177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
524182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
524183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
524183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
524184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
526695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
527535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
527538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
527539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
527539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
527539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
530072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
530906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
530910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
530911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
530911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
530912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
533423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
534260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
534263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
534266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
534266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
534266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
536797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
537614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
537618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
537620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
537620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
537620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
540152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
540990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
541003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms 
541005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
541005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
541005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
543534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
544350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
544364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
544365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
544366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
544366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
546898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
547736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
547746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
547747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
547747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
547748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
550260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
551100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
551110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
551112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
551112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.6ns 
551113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
553648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
554483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
554506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.18ms 
554507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
554508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
554508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
557011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
557848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
557871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms 
557874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
557874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.3ns 
557875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
560408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
561244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
561266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.58ms 
561267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
561267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
561268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
563800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
564614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
564627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
564628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
564628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
564629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
567161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
567999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
568027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.83ms 
568028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
568028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
568029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
570557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
571398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
571442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.53ms 
571443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
571443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
571444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
573958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
574794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
574829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.97ms 
574831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
574831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
574831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
577364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
578200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
578239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.61ms 
578240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
578240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
578241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
580754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
581589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
581630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.28ms 
581632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
581632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
581633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
584160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
584996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
585106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.04ms 
585107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
585107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
585108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
587644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
588483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
588491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
588492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
588492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
588493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
591006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
591843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
591850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
591851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
591851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
591852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
594376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
595214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
595219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
595220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
595220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
595221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
597776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
598616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
598633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
598634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
598634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
598635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
601162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
602001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
602012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.28ms 
602013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
602013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
602014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
604550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
605390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
605393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
605394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
605394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
605395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
607928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
608768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
608783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
608785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
608785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
608785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
611305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
612145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
612161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
612162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
612162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
612163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
614696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
615536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
615554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.37ms 
615556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
615557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.9ns 
615557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
618091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
618929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
618932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
618933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
618933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
618933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
621467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
622287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
622291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
622292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
622292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
622293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
624820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
625658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
625664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.36ms 
625665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
625665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
625666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
628197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
629035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
629042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
629043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
629043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
629044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
631595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
632433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
632501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.21ms 
632503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
632503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
632504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
635058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
635878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
635947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.91ms 
635954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
635955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.7ns 
635955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
638478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
639320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
639341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms 
639342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
639342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
639343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
641878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
642717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
642719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.9ns 
642721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
642721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
642722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
645258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
646097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
646281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 173.1ms 
646282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
646283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.3ns 
646283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
648824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
649667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
649715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.75ms 
649717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
649717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
649717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
652241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
653078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
653080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.2ns 
653081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
653081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
653082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
655600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
656439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
656440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.9ns 
656441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
656442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
656442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
658967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
659811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
659813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 355.3ns 
659814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
659815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
659815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
662323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
663160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
663162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 461.3ns 
663163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
663163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
663163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
665685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
666521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
666608     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
666623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.2ms 
666626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
666627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 
666627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
669175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
670020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
670072     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
670073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.43ms 
670075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
670075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
670076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
672617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
673460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
673461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
673486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
673529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
673549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
673557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
673567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
673570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
673571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
673574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
673577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
673579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
673583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
673584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
673778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
673780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
673781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
673782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
673783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
673883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
673884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
673886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
673887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
673888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
673889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
674030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
674032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
674033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
674034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
674034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
674036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
674141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
674142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
674143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
674144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
674145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
674146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
674152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
674153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
674154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
674155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
674157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
674157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
674163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
674164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
674165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
674166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
674167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
674167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
674292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
674293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
674295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
674417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
674418     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)'' 
674420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
674421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
674422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
674423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
674424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
674425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
674431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
674433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
674434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
674434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
674435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
674531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
674534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
674536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
674536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
674537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
674538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
674539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
674648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
674649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
674650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
674651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
674652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
674652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
674653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
674654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
674769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
674770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
674866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
674870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
674876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
674877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
674879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
674881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
674883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
674883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
674884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
674885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
674893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
674897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
674994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
674995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
674997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
674998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
674999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
674999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
675000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
675001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
675055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
675060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
675149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
675150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
675153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
675154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
675155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
675156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
675280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
675284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
675286     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)'' 
675288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
675289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
675290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
675292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
675293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
675301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
675307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
675308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
675309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
675400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
675401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
675402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
675403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
675404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
675405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
675500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
675502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
675503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
675505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
675505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
675506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
675506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
675507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
675588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
675590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
675664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
675664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
675665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
675670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
675674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
675678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
675823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
675824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
675825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
675826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
675837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
675926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
679453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
679454     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)'' 
679459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
679460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
679460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
679461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
679462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
679469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
679471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
679472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
679472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
679473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
679564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
679568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
679569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
679570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
679570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
679571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
679572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
679665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
679666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
679667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
679668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
679669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
679670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
679670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
679671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
679744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
679746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
679817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
679822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
679826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
679827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
679828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
679829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
679838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
679915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
679917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
679918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
679919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
679990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
679999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
680000     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)'' 
680002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
680003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
680004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
680004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
680005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
680015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
680017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
680018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
680018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
680019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
680104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
680106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
680107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
680107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
680108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
680195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
680200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
680201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
680201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
680202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
680203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
680203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
680301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
680303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
680304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
680305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
680306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
680306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
680307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
680308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
680309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
680310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
680311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
680311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
680312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
680312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
680313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
680398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
680399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
680405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
680482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
680562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
680564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
680565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
680566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
680567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
680567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
680568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
680569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
680570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
680654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
680660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
680746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
680747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
680748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
680749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
680749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
680749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
680750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
680750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
680755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
680756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
680833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
680839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
680844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
680942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
680943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
680943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
680944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
680945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
680945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
680945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
680946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
681046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
681047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
681048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
681048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
681049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
681054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
681059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
681170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
681254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
681255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
681256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
681257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
681417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
681501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
681502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
684467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
684471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
684472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
684473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
684474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
684628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
684630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
684631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
684631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
684632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
684733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
687599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
690722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
690727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
690728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
690728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
690729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
690839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
690840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
690841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
690842     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)' ...' 
690843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
691966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
691966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
691967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
694569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
695433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
695434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
695435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
695443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
695453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
695456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
695457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
695458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
695462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
695463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
695467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
695469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
695470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
695479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
695480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
695481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
695540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
695541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
695542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
695542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
695543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
695614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
695614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
695615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
695616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
695616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
695620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
695620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
695620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
695621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
695622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
695622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
695715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
695716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
695716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
695717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
695718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
695718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
695812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
695812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
695813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
695813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
695814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
695815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
695815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
695815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
695816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
695816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
695817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
695817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
695817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
695818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
695818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
695818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
695819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
695820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
695820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
695822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
695862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
695863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
695925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
695925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
695927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
695928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
695928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
695929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
695983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
695986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
695987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
695988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
695989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
695990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
695990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
696047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
696049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
696052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
696112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
696174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
696174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
696175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
698749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
699619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
699649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.94ms