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

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

tests
0

failures
0

ignored
11m27.73s

duration
100%

successful

Tests

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

Standard output

653        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
679        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.94ms 
921        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
935        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)

1781       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1783       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1786       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1786       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3581       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9253       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.33s 
9330       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9378       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
9395       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9396       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 910.61ns 
9402       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
12383      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13490      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.03ms 
13501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.4ns 
13503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
16464      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17406      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.5ms 
17410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
17411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
20264      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21222      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
21228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.71ns 
21230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
23866      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
24765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
24781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 594.81ns 
24783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27412      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
27413      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28289      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.82ms 
28295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.91ns 
28297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
30895      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31757      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
31763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.11ns 
31765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
34323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
35182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
35186      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.61ns 
35189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
35190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.61ns 
35191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
37769      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
38620      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
38624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
38624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
38625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
41209      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
42049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
42052      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.21ns 
42055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
42055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348ns 
42057      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44609      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
44609      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
45500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
45504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.11ns 
45507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
45508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.57ms 
45509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48080      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
48081      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.32ns 
48927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.91ns 
48929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
51485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
52328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
52384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.86ms 
52390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
52390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.3ns 
52391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
54929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55839      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.42ms 
55841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns 
55842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
58410      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
59244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
59384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.29ms 
59388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
59388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.71ns 
59389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
61936      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
62777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
62778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
65318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
66175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
66179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
66183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
66183      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.41ns 
66185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
68744      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
69583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69645      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.24ms 
69649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69649      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
69650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
72227      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
73057      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
73070      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
73071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
73072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.3ns 
73072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
75637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
76444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
76456      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
76459      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
76460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.5ns 
76461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
79006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79847      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
79849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.71ns 
79851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82391      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
82391      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
83217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
83229      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
83230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
83231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
83232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
85788      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86618      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.75ms 
86620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.1ns 
86621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
89157      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89983      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
89984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
89985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
92510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
93349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
93386      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.37ms 
93390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
93393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.79ms 
93394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
95936      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96785      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.68ms 
96788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96788      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.91ns 
96789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
99336      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
100161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
100191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms 
100193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
100193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
100194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
102701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
103539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
103540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
106080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
106888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
106889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
109401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.59ms 
110231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
110232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
112719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
113554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 
113555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
116085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
116901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.11ns 
116902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
119438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
120271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
120272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
122826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
123664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
123665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
126209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
127036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
127046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
127048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
127048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.8ns 
127049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
129582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.24ms 
130447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.5ns 
130461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
133037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
133862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
133882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
133886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
133886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.6ns 
133888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
136441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
137288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.5ns 
137289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
139821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
140665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.11ns 
140667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
143184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
144008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
144022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.23ms 
144024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
144024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
144025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
146578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.99ms 
147439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126ns 
147440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
149981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
150809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
150812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
150813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
150813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
150814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
153374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
154179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
154184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
154187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
154187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 
154188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
156738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
157571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
157572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
160099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
160924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
160931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
160933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
160933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
160934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
163483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
164297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
164298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
166846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
167679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
167686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
167687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
167688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
167688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
170195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
171015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
171018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
171020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
171020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.4ns 
171021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
173541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
174339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
174343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
174345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
174345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
174345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
176869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
177695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
177699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
177717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
177717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.61ns 
177719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
180223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
181043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
181095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.22ms 
181097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
181097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
181098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
183620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
184480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.96ms 
184482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
184482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
184483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
187001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
187823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
187826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
187828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
187828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
187829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
190318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
191162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
191191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.42ms 
191193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
191193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
191194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
193718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
194551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
194588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.9ms 
194592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
194592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.3ns 
194593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
197095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
197942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
197945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
197953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
197954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.21ns 
197955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
200461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
201278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
201380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.59ms 
201382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
201382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
201383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
203913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
204740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
204761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.19ms 
204764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
204764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.1ns 
204768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
207306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
208125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
208141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
208143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
208144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.5ns 
208145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
210679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
211474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
211490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.66ms 
211491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
211491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
211492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
214013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
214833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
214847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
214849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
214850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
214850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
217368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
218188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
218192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
218194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
218194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
218195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
220726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
221524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
221528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
221530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
221530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
221531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
224076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
224899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
224915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
224917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
224917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
224918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
227454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
228280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
228293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
228297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
228298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.1ns 
228303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
230829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
231622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
231634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ms 
231635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
231636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
231636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
234143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
234964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
234968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
234970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
234970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
234971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
237492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
238314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
238317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
238318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
238319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
238319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
240838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
241632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
241638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
241639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
241639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
241640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
244175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
244993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
244996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.81ns 
244998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
244998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
244998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
247492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
248309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
248311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.81ns 
248312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
248313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
248313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
250824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
251617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
251621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
251622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
251622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
251623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
254144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
254962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
254965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 788.41ns 
254966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
254966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
254967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
257453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
258276     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 56.09ms 
258339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
258340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.4ns 
258341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
260864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
261659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
261691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.18ms 
261693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
261693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
261694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
264238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
265058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
265082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
265083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
265083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
265084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
267591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
268410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
268442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.96ms 
268443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
268443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
268444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
270949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
271775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
271797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.58ms 
271799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
271799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
271800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
274323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
275144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
275180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.11ms 
275182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
275182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
275183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
277689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
278508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
278526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
278528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
278528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
278529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
281051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
281867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
281881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ms 
281883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
281883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
281883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
284376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
285195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
285211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
285213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
285213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
285213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
287727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
288523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
288537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
288539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
288539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
288540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
291061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
291878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
291896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
291897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
291898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
291898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
294393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
295213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
295231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
295232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
295232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
295233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
297755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
298550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
298568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
298570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
298570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
298571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
301126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
301947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
301964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 
301966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
301966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
301967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
304467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
305290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
305306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
305307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
305307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
305308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
307843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
308642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
308659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
308660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
308660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
308661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
311191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
312016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
312033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
312034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
312034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
312035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
314525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
315375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
315384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
315387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
315387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.4ns 
315388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
317902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
318697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
318709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.36ms 
318710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
318710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
318711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
321237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
322060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
322064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
322065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
322065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
322066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
324567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
325391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
325395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
325396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
325396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
325397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
327910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
328708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
328711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.31ns 
328712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
328712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
328713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
331219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
332037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
332043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
332044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
332044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
332045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
334526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
335344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
335350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
335351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
335351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
335352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
337856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
338685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
338696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
338698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
338699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.2ns 
338699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
341184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
342004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
342008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
342009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
342009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
342010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
344492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
345323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
345325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.9ns 
345327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
345327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
345328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
347816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
348636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
348641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
348643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
348643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
348644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
351118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
351938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
351940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.01ns 
351942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
351942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
351943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
354426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
355247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
355249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.11ns 
355251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
355251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
355252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
357760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
358580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
358582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.61ns 
358583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
358583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
358584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
361073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
361895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
361899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
361900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
361900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
361901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
364399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
365230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
365237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
365239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
365239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
365239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
367758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
368587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
368590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
368592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
368592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
368593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
371108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
371930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
371936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
371938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
371938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
371938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
374454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
375259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
375264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
375266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
375267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 
375267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
377783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
378601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
378614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
378615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
378615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
378616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
381097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
381917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
381920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
381921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
381922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
381922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
384416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
385236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
385239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
385241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
385241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
385242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
387725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
388544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
388548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
388549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
388550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
388550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
391061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
391854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
391868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
391869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
391869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
391870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
394382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
395200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
395204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.2ns 
395207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
395207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
395207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
397712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
398526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
398553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
398554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
398554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
398555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
401058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
401881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
401884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
401886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
401886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
401887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
404387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
405205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
405220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
405221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
405221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
405222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
407732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
408546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
408560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
408562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
408562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
408563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
411031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
411847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
411865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.13ms 
411867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
411867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
411867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
414351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
415164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
415166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.8ns 
415167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
415168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
415168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
417638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
418453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
418459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
418461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
418461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
418462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
420971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
421791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
421794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
421796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
421796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
421797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
424277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
425095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
425098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.2ns 
425099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
425099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
425100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
427602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
428427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
428430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.1ns 
428431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
428431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
428432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
430922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
431747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
431751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
431752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
431752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
431753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
434296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
435138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
435143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
435145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
435145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
435146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
437652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
438455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
438463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
438464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
438464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
438465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
440953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
441774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
441781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
441789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
441790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 534.3ns 
441790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
444317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
445140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
445146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
445148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
445148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
445149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
447653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
448484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
448496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.96ms 
448498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
448498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.8ns 
448499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
451009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
451839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
451843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
451845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
451845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
451846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
454343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
455150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
455154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
455156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
455156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
455157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
457673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
458506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
458509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.41ns 
458510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
458510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
458511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
461028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
461858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
461861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
461862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
461863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
461863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
464368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
465178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
465181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.81ns 
465185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
465185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.3ns 
465186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
467711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
468541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
468550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
468552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
468552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
468553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
471069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
471907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
471910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
471911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
471911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
471912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
474438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
475249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
475255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
475256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
475256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
475257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
477766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
478595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
478598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.9ns 
478599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
478599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
478600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
481093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
481924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
481926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.9ns 
481927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
481928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
481928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
484452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
485286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
485289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
485291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
485291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.8ns 
485291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
487821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
488634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
488636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.01ns 
488638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
488638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
488639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
491176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
492012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
492015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
492016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
492016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
492017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
494563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
495415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
495419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
495421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
495421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 
495422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
497960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
498800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
498804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
498806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
498806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
498807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
501331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
502172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
502174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.3ns 
502176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
502176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
502177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
504685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
505518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
505527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
505529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
505529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
505530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
508062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
508900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
508902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.31ns 
508904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
508904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
508904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
511428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
512261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
512267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
512269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
512269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
512270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
514794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
515628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
515631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 970.71ns 
515632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
515632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
515633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
518154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
518988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
518991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.41ns 
518992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
518992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
518993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
521510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
522343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
522347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
522349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
522349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
522349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
524888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
525735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
525739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.01ns 
525742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
525742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.7ns 
525743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
528297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
529108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
529111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
529113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
529113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
529114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
531620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
532448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
532451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
532453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
532453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.5ns 
532454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
534955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
535785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
535789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
535790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
535791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
535791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
538303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
539132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
539140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
539141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
539142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
539143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
541638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
542471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
542480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
542481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
542481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
542482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
544966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
545793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
545799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
545801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
545801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
545802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
548288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
549122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
549129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
549130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
549130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
549131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
551621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
552450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
552460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
552462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
552462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
552463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
554951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
555779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
555789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
555790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
555791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
555791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
558286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
559115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
559125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
559126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
559127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
559127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
561620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
562447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
562454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
562456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
562456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
562457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
564949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
565778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
565798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.36ms 
565799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
565799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
565800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
568285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
569112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
569133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.63ms 
569135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
569135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
569136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
571639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
572471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
572491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
572493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
572493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
572493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
574991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
575818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
575837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
575838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
575839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
575839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
578340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
579169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
579189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.85ms 
579190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
579191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
579191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
581689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
582516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
582563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.64ms 
582565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
582565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
582565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
585062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
585899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
585906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
585908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
585908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
585909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
588406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
589235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
589240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
589241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
589241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
589242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
591736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
592568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
592572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
592574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
592574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
592574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
595090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
595919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
595931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
595933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
595933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
595934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
598428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
599257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
599264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
599265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
599265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
599266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
601769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
602597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
602600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
602601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
602601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
602602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
605106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
605938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
605948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
605950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
605950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
605951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
608470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
609302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
609313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
609314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
609314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
609315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
611820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
612656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
612669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
612671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
612671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
612672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
615171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
616006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
616009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
616010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
616010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
616011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
618528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
619356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
619359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
619361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
619361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
619362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
621877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
622708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
622714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
622715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
622716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
622716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
625216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
626045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
626051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
626052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
626052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
626053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
628549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
629389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
629457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.93ms 
629458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
629458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
629459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
631978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
632815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
632834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.16ms 
632835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
632835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
632836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
635354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
636189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
636201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
636202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
636202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
636203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
638751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
639586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
639588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 352ns 
639590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
639590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
639591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
642123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
642957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
643036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.92ms 
643038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
643038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
643039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
645579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
646411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
646444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.17ms 
646445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
646445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
646446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
648955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
649787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
649789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219ns 
649793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
649793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248ns 
649794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
652324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
653155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
653157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 250.2ns 
653159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
653159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
653160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
655649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
656479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
656481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 237.4ns 
656482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
656482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
656483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
659009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
659843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
659845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360.6ns 
659847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
659847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
659847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
662358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
663186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
663279     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
663288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.6ms 
663291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
663291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.9ns 
663292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
665848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
666681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
666729     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
666731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.16ms 
666732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
666732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
666733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
669277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
670118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
670120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
670149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
670209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
670230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
670237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
670253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
670255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
670257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
670259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
670265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
670266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
670272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
670274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
670483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
670484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
670485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
670486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
670487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
670594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
670595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
670596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
670597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
670599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
670600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
670767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
670768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
670770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
670771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
670772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
670773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
670906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
670907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
670909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
670910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
670910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
670912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
670919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
670920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
670921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
670923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
670923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
670925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
670932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
670933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
670934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
670935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
670936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
670937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
671084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
671085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
671087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
671266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
671267     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)'' 
671268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
671270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
671271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
671272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
671273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
671276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
671280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
671281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
671282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
671283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
671284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
671401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
671405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
671406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
671407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
671408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
671409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
671410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
671546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
671548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
671549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
671550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
671551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
671552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
671554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
671555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
671665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
671667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
671764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
671769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
671775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
671776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
671778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
671783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
671784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
671785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
671786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
671786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
671796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
671802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
671910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
671913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
671916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
671917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
671918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
671919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
671920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
671922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
671978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
671985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
672086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
672088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
672089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
672091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
672092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
672093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
672231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
672235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
672238     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)'' 
672240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
672241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
672242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
672243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
672244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
672257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
672262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
672263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
672264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
672386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
672387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
672388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
672389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
672390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
672391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
672546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
672547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
672548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
672550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
672551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
672552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
672552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
672553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
672636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
672638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
672728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
672729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
672730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
672735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
672739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
672744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
672866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
672867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
672875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
672876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
672887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
672970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
676577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
676579     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)'' 
676582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
676584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
676585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
676585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
676587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
676595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
676595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
676596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
676597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
676599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
676691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
676696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
676697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
676698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
676698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
676699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
676699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
676799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
676800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
676801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
676804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
676805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
676805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
676807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
676807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
676894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
676896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
676977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
676982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
676986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
676987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
676989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
676990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
677000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
677089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
677090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
677091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
677092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
677209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
677219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
677219     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)'' 
677220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
677222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
677222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
677223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
677223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
677235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
677235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
677236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
677237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
677238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
677324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
677325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
677326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
677327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
677327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
677417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
677421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
677422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
677423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
677423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
677424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
677424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
677525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
677526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
677528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
677529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
677529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
677530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
677530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
677531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
677531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
677532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
677533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
677534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
677534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
677534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
677535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
677618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
677620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
677626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
677700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
677777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
677779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
677780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
677780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
677781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
677782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
677782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
677782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
677783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
677866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
677872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
677961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
677962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
677963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
677964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
677964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
677965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
677965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
677966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
677970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
677971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
678048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
678053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
678058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
678154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
678155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
678156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
678157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
678157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
678158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
678158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
678158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
678215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
678216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
678217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
678217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
678218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
678224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
678229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
678343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
678429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
678430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
678431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
678432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
678594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
678721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
678721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
681634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
681638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
681639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
681640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
681641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
681801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
681802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
681803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
681803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
681804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
681908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
685005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
688188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
688192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
688193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
688193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
688194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
688305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
688306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
688307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
688308     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)' ...' 
688309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
689422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
689423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.3ns 
689424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
692046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
692918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
692919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
692920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
692930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
692942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
692945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
692947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
692949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
692955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
692956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
692961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
692962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
692965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
692976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
692977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
692979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
693035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
693036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
693037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
693038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
693039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
693111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
693112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
693113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
693114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
693114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
693119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
693120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
693121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
693121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
693122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
693123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
693208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
693209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
693210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
693210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
693212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
693212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
693294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
693295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
693296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
693297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
693297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
693298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
693299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
693299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
693300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
693301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
693301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
693302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
693302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
693303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
693303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
693304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
693304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
693305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
693306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
693308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
693342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
693344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
693393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
693394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
693395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
693396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
693398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
693399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
693440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
693443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
693444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
693445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
693446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
693447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
693448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
693490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
693493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
693496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
693546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
693599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
693599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
693600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
696253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
697142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
697159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms