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

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

tests
0

failures
0

ignored
10m58.26s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.146s passed
powPositiveConcrete data()[101] 3.143s passed
powGeq1Concrete data()[102] 3.154s passed
pow2InIntLower data()[103] 3.168s passed
pow2InIntUpper data()[104] 3.162s passed
logSelfConcrete data()[105] 3.178s passed
log1Concrete data()[106] 3.204s passed
logProduct data()[107] 3.192s passed
logTimesBaseConcrete data()[108] 3.165s passed
logProdIdentity data()[109] 3.176s passed
moduloByteIsInByte data()[10] 3.216s passed
logProdIdentityConcrete data()[110] 3.168s passed
logPowIdentity data()[111] 3.184s passed
logPowIdentityConcrete data()[112] 3.161s passed
logPositive data()[113] 3.177s passed
logPositiveConcrete data()[114] 3.185s passed
logMono data()[115] 3.195s passed
logMonoConcrete data()[116] 3.175s passed
powLogLess data()[117] 3.201s passed
powLogMore2 data()[118] 3.166s passed
logLessThanPow data()[119] 3.205s passed
moduloCharIsInChar data()[11] 3.237s passed
logLessThanPowConcrete data()[120] 3.194s passed
logSqueeze data()[121] 3.175s passed
ifthenelse_equals data()[122] 3.153s passed
ifthenelse_equals_1 data()[123] 3.150s passed
ifthenelse_equals_2 data()[124] 3.182s passed
disjointWithSingleton1 data()[125] 3.203s passed
disjointWithSingleton2 data()[126] 3.143s passed
disjointArrayRanges data()[127] 3.204s passed
disjointArrayRangeAllFields1 data()[128] 3.250s passed
disjointArrayRangeAllFields2 data()[129] 3.189s passed
div_unique1 data()[12] 3.304s passed
seqSelfDefinition data()[130] 3.185s passed
seqOutsideValue data()[131] 3.227s passed
castedGetAny data()[132] 3.209s passed
seqGetAlphaCast data()[133] 3.266s passed
getOfSeqSingleton data()[134] 3.161s passed
getOfSeqSingletonConcrete data()[135] 3.183s passed
getOfSeqConcat data()[136] 3.232s passed
getOfSeqSub data()[137] 3.217s passed
getOfSeqReverse data()[138] 3.191s passed
lenOfSeqEmpty data()[139] 3.176s passed
div_unique2 data()[13] 3.365s passed
lenOfSeqSingleton data()[140] 3.180s passed
lenOfSeqConcat data()[141] 3.136s passed
lenOfSeqSub data()[142] 3.147s passed
lenOfSeqReverse data()[143] 3.175s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.154s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.163s passed
getOfSeqSingletonEQ data()[146] 3.197s passed
getOfSeqConcatEQ data()[147] 3.184s passed
getOfSeqSubEQ data()[148] 3.161s passed
getOfSeqReverseEQ data()[149] 3.192s passed
div_exists data()[14] 3.461s passed
lenOfSeqEmptyEQ data()[150] 3.191s passed
lenOfSeqSingletonEQ data()[151] 3.172s passed
lenOfSeqConcatEQ data()[152] 3.189s passed
lenOfSeqSubEQ data()[153] 3.159s passed
lenOfSeqReverseEQ data()[154] 3.152s passed
getOfSeqDefEQ data()[155] 3.173s passed
lenOfSeqDefEQ data()[156] 3.160s passed
seqConcatWithSeqEmpty1 data()[157] 3.187s passed
seqConcatWithSeqEmpty2 data()[158] 3.168s passed
seqReverseOfSeqEmpty data()[159] 3.160s passed
div_one data()[15] 3.271s passed
subSeqComplete data()[160] 3.192s passed
subSeqTailR data()[161] 3.196s passed
subSeqTailL data()[162] 3.192s passed
subSeqTailEQR data()[163] 3.229s passed
subSeqTailEQL data()[164] 3.199s passed
seqDef_split data()[165] 3.223s passed
seqDef_induction_upper data()[166] 3.216s passed
seqDef_induction_upper_concrete data()[167] 3.200s passed
seqDef_induction_lower data()[168] 3.216s passed
seqDef_induction_lower_concrete data()[169] 3.217s passed
jdiv_one data()[16] 3.233s passed
seqDef_split_in_three data()[170] 3.289s passed
seqDef_empty data()[171] 3.157s passed
seqDef_one_summand data()[172] 3.149s passed
seqDef_lower_equals_upper data()[173] 3.148s passed
seqDefOfSeq data()[174] 3.156s passed
seqSelfDefinitionEQ2 data()[175] 3.182s passed
indexOfSeqSingleton data()[176] 3.178s passed
indexOfSeqConcatFirst data()[177] 3.163s passed
indexOfSeqConcatSecond data()[178] 3.169s passed
indexOfSeqSub data()[179] 3.174s passed
div_zero data()[17] 3.314s passed
lenOfArray2seq data()[180] 3.174s passed
getAnyOfArray2seq data()[181] 3.174s passed
getOfArray2seq data()[182] 3.167s passed
getAnyOfNPermInv data()[183] 3.156s passed
seqNPermRange data()[184] 3.219s passed
seqPermTrans data()[185] 3.206s passed
seqPermRefl data()[186] 3.151s passed
seqPermSplit data()[187] 3.182s passed
seqNPermRight data()[188] 3.354s passed
seqPermFromSwap data()[189] 3.245s passed
divResZero1 data()[18] 3.247s passed
seqPermTransAlt0 data()[190] 3.169s passed
seqPermTransAlt1 data()[191] 3.145s passed
seqPermTransAlt2 data()[192] 3.164s passed
seqPermTransAlt3 data()[193] 3.164s passed
seqPermForall data()[194] 3.243s passed
seqPermExists data()[195] 3.218s passed
schiffl_lemma_2 data()[196] 22.676s passed
schiffl_thm_1 data()[197] 3.998s passed
eqSameSeq data()[198] 3.211s passed
divResZero2 data()[19] 3.236s passed
eqTermCut data()[1] 4.132s passed
divResOne1 data()[20] 3.246s passed
divResOne2 data()[21] 3.261s passed
div_cancel1 data()[22] 3.258s passed
div_cancel2 data()[23] 3.213s passed
divAddMultDenom data()[24] 3.217s passed
divMinus data()[25] 3.271s passed
divMinusDenom data()[26] 3.258s passed
divLeastDPos data()[27] 3.214s passed
divLeastDNeg data()[28] 3.195s passed
divGreatestDPos data()[29] 3.193s passed
equivAllRight data()[2] 3.797s passed
divGreatestDNeg data()[30] 3.207s passed
divIncreasingPos data()[31] 3.203s passed
divIncreasingNeg data()[32] 3.204s passed
jdiv_zero data()[33] 3.217s passed
jdivPulloutMinusNum data()[34] 3.228s passed
jdivPulloutMinusDenom data()[35] 3.266s passed
jdiv_uniquePosPos data()[36] 3.252s passed
jdiv_uniquePosNeg data()[37] 3.220s passed
jdiv_uniqueNegPos data()[38] 3.227s passed
jdiv_uniqueNegNeg data()[39] 3.207s passed
irrflConcrete1 data()[3] 3.725s passed
jdivMultDenom1 data()[40] 3.223s passed
jdivMultDenom2 data()[41] 3.285s passed
mod_geZero data()[42] 3.229s passed
mod_lessDenom data()[43] 3.249s passed
jmod_NumPos data()[44] 3.183s passed
jmod_NumNeg data()[45] 3.227s passed
jmod_geZero data()[46] 3.252s passed
jmodNumZero data()[47] 3.191s passed
jmod_pulloutminusNum data()[48] 3.216s passed
jmod_pulloutminusDenom data()[49] 3.186s passed
irrflConcrete2 data()[4] 3.564s passed
jmodUnique1 data()[50] 3.269s passed
jmodUnique2 data()[51] 3.339s passed
intDivRem data()[52] 3.213s passed
jmodjmod data()[53] 3.231s passed
jmodDivisible data()[54] 3.290s passed
jmodDivisibleRep data()[55] 3.226s passed
jdivAddMultDenom data()[56] 3.390s passed
jmodAltZero data()[57] 3.191s passed
jmodAddMultDenomZero data()[58] 3.181s passed
polyDiv_zero data()[59] 3.165s passed
cancel_gtPos data()[5] 3.522s passed
polyMod_ltdivDenom data()[60] 3.249s passed
bsum_empty data()[61] 3.181s passed
bsum_induction_upper data()[62] 3.200s passed
bsum_induction_lower data()[63] 3.257s passed
bsum_num_of_bounds data()[64] 3.292s passed
bsum_num_of_bounds2 data()[65] 3.217s passed
bsum_induction_upper2 data()[66] 3.212s passed
bsum_induction_upper_concrete data()[67] 3.198s passed
bsum_induction_upper_concrete_2 data()[68] 3.198s passed
bsum_induction_upper2_concrete data()[69] 3.183s passed
cancel_gtNeg data()[6] 3.409s passed
bsum_induction_lower_concrete data()[70] 3.193s passed
bsum_induction_lower2 data()[71] 3.187s passed
bsum_induction_lower2_concrete data()[72] 3.191s passed
bsum_positive data()[73] 3.260s passed
bsum_upper_bound data()[74] 3.204s passed
bsum_lower_bound data()[75] 3.230s passed
bsum_positive_lower_bound_element data()[76] 3.267s passed
bsum_sub_same_index data()[77] 3.230s passed
bsum_less_same_index data()[78] 3.263s passed
bsum_equal_except_one_index data()[79] 3.257s passed
moduloIntIsInInt data()[7] 3.247s passed
bsum_num_of_is_max data()[80] 3.356s passed
bsum_num_of_is_max2 data()[81] 3.198s passed
bsum_num_of_is_max3 data()[82] 3.222s passed
bsum_num_of_is_max4 data()[83] 3.243s passed
bsum_num_of_lt_max data()[84] 3.200s passed
bsum_num_of_lt_max2 data()[85] 3.236s passed
bsum_num_of_lt_max3 data()[86] 3.214s passed
bsum_num_of_lt_max4 data()[87] 3.203s passed
bsum_num_of_gt0 data()[88] 3.221s passed
bsum_num_of_gt0_alt data()[89] 3.178s passed
moduloLongIsInLong data()[8] 3.207s passed
bsum_add_concrete data()[90] 3.174s passed
bprod_all_positive data()[91] 3.215s passed
bprod_split data()[92] 3.180s passed
powConcrete0 data()[93] 3.185s passed
powConcrete1 data()[94] 3.188s passed
powSplitFactor data()[95] 3.233s passed
powAdd data()[96] 3.175s passed
powMono data()[97] 3.148s passed
powMonoConcrete data()[98] 3.156s passed
powMonoConcreteRight data()[99] 3.141s passed
moduloShortIsInShort data()[9] 3.293s passed

Standard output

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

1623       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1625       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1629       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1629       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2964       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8244       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.59s 
8322       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8354       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.6ns 
8366       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8366       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195ns 
8370       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
11385      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12489      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.01ms 
12502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 
12504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
15351      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
16299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.2ns 
16301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
19030      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20022      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
20024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.9ns 
20026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22682      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
22682      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23587      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
23591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 689.4ns 
23594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26209      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
26210      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27107      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.32ms 
27114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 610.29ns 
27116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
29670      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.78ms 
30524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.4ns 
30525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
32986      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.5ns 
33772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.2ns 
33773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
36204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619ns 
36978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193ns 
36979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
39481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40269      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.5ns 
40271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313ns 
40272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
42684      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.5ns 
43487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.1ns 
43489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
45926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46721      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535ns 
46725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.1ns 
46726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
49182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.37ms 
50028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
50029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52495      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
52495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53391      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.32ms 
53393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
53394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
55830      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56851      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 234.66ms 
56854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.8ns 
56856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
59327      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
60125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 
60127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
62589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63356      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
63358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63358      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns 
63359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
65820      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66670      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.29ms 
66673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.4ns 
66675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
69105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69918      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.35ms 
69920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
69921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72349      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
72349      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
73156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.3ns 
73157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75599      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
75599      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76385      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76400      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 
76402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.3ns 
76404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
78858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
79663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
79664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
82121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82919      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
82921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82921      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns 
82922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
85366      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86132      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
86133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
86135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
88529      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.96ms 
89351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89351      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 
89352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
91758      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92620      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.01ms 
92622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.7ns 
92624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
95037      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.77ms 
95880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
95881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
98296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
99094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 
99095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
101489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
102293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
102294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
104708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
105486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
105486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
107928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
108692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
108693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
111120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
111896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
111897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
114311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
115099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
115100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
117521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
118316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
118317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
120707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
121545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.9ns 
121546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
123965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
124809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.36ms 
124811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.5ns 
124812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
127228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.15ms 
128063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 
128064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
130506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms 
131282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
131283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
133711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
134509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
134510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
136909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
137694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
137715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
137717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
137717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 
137718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
140106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
140898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
140938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.34ms 
140941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
140941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
140942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
143419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 977.3ns 
144225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
144226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
146648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
147453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
147454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
149895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
150697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
150703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.2ns 
150704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
153117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
153876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
153884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
153886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
153886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
153886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
156303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.06ms 
157112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.5ns 
157114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
159568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
160365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
160366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
162759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
163555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.5ns 
163556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
165983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
166766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
166770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
166772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
166772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
166773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
169173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
169956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
169957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
169958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
169958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
172370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
173225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.66ms 
173227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
173228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
175690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
176447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
176564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.3ms 
176565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
176565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
176566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
178988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
179772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
179777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
179779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
179779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
179780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
182198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.44ms 
183010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.9ns 
183011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
185438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
186251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
186298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.68ms 
186301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
186301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251ns 
186302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
188692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
189521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
189524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
189525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
189525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
189526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
191962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
192747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
192914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 154.18ms 
192915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
192916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
192916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
195308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
196095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
196106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
196107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
196107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
196108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
198498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
199277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
199286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
199288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
199288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 
199289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
201679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
202436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
202452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 
202453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
202453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
202454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
204921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
205688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
205700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
205702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
205702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
205703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
208126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
208878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
208882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
208883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
208883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
208884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
211282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
212077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
212081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
212083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
212083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
212084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
214524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
215307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
215334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
215341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
215342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.8ns 
215343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
217798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
218615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
218631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
218632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
218633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
218633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
221052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
221833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
221849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
221850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
221850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
221851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
224270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
225057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
225061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
225062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
225062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
225063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
227469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
228254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
228258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
228260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
228260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
228261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
230696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
231451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
231456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
231457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
231457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
231458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
233846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
234636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
234639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
234641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
234641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
234641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
237043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
237830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
237832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.4ns 
237835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
237835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
237835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
240236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
241016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
241020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
241021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
241021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.6ns 
241022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
243406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
244208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
244210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.6ns 
244212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
244212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
244212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
246616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
247397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
247470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.16ms 
247472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
247472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
247473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
249878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
250637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
250674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.95ms 
250675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
250675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
250676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
253109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
253868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
253904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.56ms 
253906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
253906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
253907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
256323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
257129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
257171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.68ms 
257173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
257173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns 
257174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
259589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
260373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
260401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ms 
260402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
260402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
260403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
262819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
263616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
263664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.93ms 
263665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
263665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
263666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
266090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
266890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
266921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.79ms 
266923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
266923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.7ns 
266924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
269433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
270258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
270278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ms 
270279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
270279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
270280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
272664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
273448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
273474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.58ms 
273477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
273477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
273478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
275903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
276678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
276697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.34ms 
276698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
276698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
276699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
279149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
279913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
279940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.39ms 
279941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
279941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
279942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
282332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
283115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
283140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.12ms 
283141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
283142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
283142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
285520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
286344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
286376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.61ms 
286378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
286378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
286381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
288790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
289566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
289590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.48ms 
289591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
289591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
289592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
291975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
292772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
292793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.5ms 
292794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
292794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
292795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
295197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
295981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
296015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.01ms 
296016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
296016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
296016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
298412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
299168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
299192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.39ms 
299193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
299193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
299194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
301600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
302359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
302367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
302368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
302368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
302369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
304806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
305565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
305582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
305583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
305583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
305584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
307973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
308757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
308762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
308763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
308763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
308764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
311161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
311943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
311946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
311948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
311948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.7ns 
311949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
314334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
315131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
315134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.9ns 
315136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
315136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
315137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
317579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
318360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
318367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
318369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
318369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.2ns 
318370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
320752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
321535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
321542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
321543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
321544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.3ns 
321544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
323926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
324679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
324691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
324692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
324692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
324693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
327091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
327843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
327846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
327847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
327847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
327848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
330211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
330985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
330987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.9ns 
330988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
330988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
330989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
333352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
334128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
334133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
334134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
334134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
334135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
336494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
337274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
337276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.8ns 
337277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
337278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
337278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
339651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
340429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
340431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.3ns 
340432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
340432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
340433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
342817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
343596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
343598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.4ns 
343599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
343599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
343600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
345989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
346757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
346761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
346762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
346762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
346762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
349170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
349930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
349939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.77ms 
349940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
349940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
349941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
352351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
353139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
353142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
353144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
353144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
353144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
355542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
356328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
356335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
356336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
356336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
356337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
358707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
359495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
359499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
359500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
359500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
359501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
361879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
362658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
362675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
362676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
362676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
362677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
365065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
365840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
365844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
365845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
365845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
365845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
368252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
369024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
369027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
369028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
369028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
369029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
371430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
372184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
372188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
372189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
372189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
372190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
374572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
375349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
375365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
375367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
375368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 532.4ns 
375369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
377773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
378546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
378550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495.7ns 
378552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
378553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns 
378553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
380936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
381706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
381745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.89ms 
381747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
381747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
381747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
384143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
384916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
384920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
384923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
384923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns 
384924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
387322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
388101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
388122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.52ms 
388123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
388123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
388124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
390504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
391268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
391289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
391290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
391290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
391291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
393704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
394458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
394492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.33ms 
394495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
394495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.4ns 
394496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
396919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
397686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
397688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.7ns 
397689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
397689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
397690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
400076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
400857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
400862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
400863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
400863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
400864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
403235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
404013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
404015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
404016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
404016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
404017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
406382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
407163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
407166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.1ns 
407167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
407167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
407167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
409551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
410345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
410347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 940.9ns 
410348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
410348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
410349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
412753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
413519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
413551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
413552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
413552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
413553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
415936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
416691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
416693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
416695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
416695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
416695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
419110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
419888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
419897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms 
419898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
419898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
419899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
422354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
423135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
423147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
423149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
423149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
423150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
425533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
426320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
426335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.26ms 
426338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
426338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
426338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
428716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
429505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
429521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
429524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
429524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.4ns 
429525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
431924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
432745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
432749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
432751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
432751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
432751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
435154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
435953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
435959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
435960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
435960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
435960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
438438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
439223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
439225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.3ns 
439226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
439226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
439227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
441619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
442382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
442385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
442386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
442386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
442387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
444769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
445566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
445568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.8ns 
445569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
445569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
445570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
448000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
448789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
448800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
448801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
448801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
448802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
451213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
452013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
452017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
452019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
452019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
452019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
454411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
455202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
455208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
455209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
455210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
455210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
457593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
458382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
458384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762ns 
458385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
458385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
458386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
460781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
461562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
461564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.5ns 
461565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
461565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
461566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
463936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
464697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
464700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
464701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
464701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
464702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
467087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
467845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
467848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
467849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
467849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
467849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
470230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
471020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
471023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
471024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
471024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
471024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
473401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
474173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
474176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
474177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
474177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
474178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
476546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
477334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
477339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
477340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
477340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
477341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
479745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
480534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
480537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
480538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
480538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
480539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
482931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
483710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
483721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.24ms 
483722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
483722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
483723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
486088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
486879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
486882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.2ns 
486883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
486883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
486883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
489275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
490067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
490073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
490075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
490075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
490075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
492475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
493262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
493265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.6ns 
493266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
493266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179ns 
493267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
495647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
496435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
496437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.6ns 
496438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
496438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
496439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
498836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
499620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
499625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
499626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
499626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
499627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
501996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
502780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
502784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
502786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
502786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns 
502787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
505151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
505934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
505937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
505938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
505938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
505939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
508305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
509105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
509109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
509110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
509110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
509111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
511483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
512265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
512269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
512270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
512270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
512271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
514662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
515443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
515457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.25ms 
515458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
515458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
515458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
517812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
518596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
518624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.31ms 
518625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
518625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
518626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
520988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
521774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
521784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
521786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
521786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
521786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
524194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
524965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
524976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
524978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
524979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.43ms 
524980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
527354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
528147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
528173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.9ms 
528174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
528174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
528174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
530577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
531340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
531365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.7ms 
531366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
531366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
531367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
533761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
534534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
534593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.3ms 
534594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
534594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
534595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
536962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
537776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
537793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
537794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
537794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
537795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
540192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
540983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
541015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.43ms 
541017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
541017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
541018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
543402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
544183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
544231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.88ms 
544233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
544233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
544233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
546601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
547390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
547431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.36ms 
547433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
547433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178ns 
547434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
549819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
550606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
550648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.24ms 
550649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
550649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
550650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
553060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
553820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
553864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.62ms 
553865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
553865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
553866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
556244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
557031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
557153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.81ms 
557154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
557154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
557155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
559519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
560303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
560311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
560312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
560312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
560313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
562662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
563452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
563460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
563461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
563461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
563461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
565821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
566602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
566607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
566608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
566609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
566609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
568983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
569746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
569763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
569765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
569765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
569765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
572164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
572934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
572946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.02ms 
572947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
572947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
572947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
575335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
576120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
576123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
576125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
576125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
576125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
578491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
579271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
579287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
579288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
579288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
579289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
581646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
582436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
582455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.56ms 
582457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
582457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
582458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
584848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
585610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
585629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
585630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
585630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
585631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
588006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
588801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
588803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.7ns 
588804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
588805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
588805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
591190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
591974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
591977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
591978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
591978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
591979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
594358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
595139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
595145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
595146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
595146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
595146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
597533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
598294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
598300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
598301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
598301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
598302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
600669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
601451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
601520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.55ms 
601521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
601521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
601522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
603905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
604699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
604726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.1ms 
604727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
604727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
604728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
607073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
607855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
607876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.52ms 
607878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
607878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
607878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
610272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
611056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
611058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.4ns 
611061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
611061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
611062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
613434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
614216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
614413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.18ms 
614415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
614415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.3ns 
614416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
616843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
617609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
617659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.14ms 
617660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
617660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
617661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
620044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
620826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
620828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.5ns 
620830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
620830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.8ns 
620831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
623188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
623971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
623973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 330.6ns 
623974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
623974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
623975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
626367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
627135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
627137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.2ns 
627138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
627138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
627139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
629516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
630299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
630301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 467.6ns 
630302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
630302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
630302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
632667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
633449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
633543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.79ms 
633545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
633546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.6ns 
633546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
635946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
636713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
636761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.09ms 
636763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
636763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
636765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
639180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
639980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
639981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
640006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
640045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
640062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
640067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
640073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
640076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
640077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
640079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
640082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
640084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
640086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
640088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
640252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
640254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
640255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
640256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
640257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
640374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
640376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
640377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
640379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
640381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
640382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
640561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
640563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
640564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
640565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
640566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
640566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
640706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
640707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
640708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
640709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
640710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
640711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
640718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
640719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
640719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
640721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
640722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
640723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
640731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
640732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
640733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
640734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
640734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
640735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
640877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
640878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
640879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
641008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
641010     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)'' 
641012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
641013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
641014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
641015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
641015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
641016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
641020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
641021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
641023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
641023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
641024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
641139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
641143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
641145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
641145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
641146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
641147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
641148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
641274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
641276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
641277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
641278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
641279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
641280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
641280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
641282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
641380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
641382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
641492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
641496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
641502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
641504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
641505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
641507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
641507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
641508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
641508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
641509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
641518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
641523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
641637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
641638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
641639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
641641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
641641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
641641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
641642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
641643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
641712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
641720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
641842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
641844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
641846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
641847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
641848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
641849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
641991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
641996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
641997     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)'' 
641999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
642000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
642000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
642001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
642002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
642011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
642013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
642014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
642015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
642123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
642125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
642126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
642126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
642127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
642128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
642261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
642263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
642264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
642265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
642266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
642266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
642267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
642268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
642405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
642407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
642487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
642488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
642489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
642493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
642497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
642501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
642654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
642655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
642656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
642657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
642675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
642845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
646535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
646536     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)'' 
646542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
646543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
646544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
646544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
646545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
646552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
646554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
646555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
646556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
646556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
646648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
646652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
646653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
646654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
646655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
646655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
646656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
646751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
646753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
646753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
646755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
646755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
646756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
646756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
646757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
646834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
646835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
646917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
646921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
646925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
646926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
646927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
646928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
646938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
647027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
647028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
647029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
647030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
647104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
647115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
647116     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)'' 
647118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
647119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
647120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
647121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
647121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
647132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
647133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
647134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
647135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
647136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
647223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
647225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
647226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
647227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
647228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
647320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
647324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
647325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
647326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
647326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
647327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
647328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
647427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
647428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
647429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
647431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
647431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
647432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
647432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
647434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
647434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
647435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
647436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
647437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
647437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
647438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
647439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
647527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
647528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
647534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
647663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
647743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
647744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
647746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
647746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
647747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
647748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
647748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
647748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
647749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
647835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
647840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
647931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
647932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
647933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
647934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
647934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
647935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
647935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
647936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
647941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
647941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
648021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
648026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
648031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
648129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
648131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
648131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
648132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
648133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
648133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
648134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
648135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
648189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
648190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
648191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
648191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
648192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
648197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
648202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
648319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
648406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
648408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
648408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
648410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
648576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
648666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
648666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
651709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
651714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
651715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
651716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
651716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
651830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
651831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
651832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
651833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
651833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
651988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
654969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
658124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
658128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
658129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
658130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
658131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
658242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
658244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
658245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
658246     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)' ...' 
658247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
659439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
659440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.6ns 
659441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
661946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
662753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
662754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
662754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
662760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
662772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
662774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
662776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
662776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
662781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
662782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
662784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
662787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
662787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
662796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
662797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
662798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
662841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
662842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
662842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
662843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
662843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
662910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
662910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
662912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
662913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
662913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
662917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
662917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
662918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
662919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
662920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
662920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
663004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
663005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
663005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
663007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
663007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
663008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
663096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
663097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
663097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
663098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
663098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
663099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
663100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
663100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
663101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
663102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
663102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
663102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
663103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
663103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
663104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
663104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
663105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
663106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
663107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
663109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
663148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
663150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
663213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
663214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
663215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
663217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
663217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
663218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
663274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
663277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
663278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
663280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
663281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
663282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
663282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
663329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
663332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
663335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
663384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
663437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
663437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.8ns 
663438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
665832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
666615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
666646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.02ms