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

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

tests
0

failures
0

ignored
10m55.81s

duration
100%

successful

Tests

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

Standard output

289        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
312        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.7ms 
544        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557        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)

1481       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1484       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1486       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1486       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2970       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7975       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.43s 
8035       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8067       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.2ns 
8080       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8082       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.76ms 
8086       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
10976      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11898      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.14ms 
11911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.2ns 
11913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
14671      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15546      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
15548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 
15552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
18177      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
19042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.1ns 
19044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
21587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
22479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 554.11ns 
22482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
25016      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25921      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.38ms 
25923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
25924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
28502      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29335      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
29339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.3ns 
29341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
31794      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32626      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.11ns 
32628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32629      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.8ns 
32630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35125      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35936      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.9ns 
35940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.6ns 
35941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
38423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39237      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.21ns 
39238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
39239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
41673      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.01ns 
42484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.9ns 
42487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
44948      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.21ns 
45760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.8ns 
45773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
48283      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49107      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.1ms 
49111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.84ms 
49114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
51561      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52366      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
52368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.3ns 
52369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54808      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
54809      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55695      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105ms 
55698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
55700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
58134      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58922      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
58925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.7ns 
58927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
61375      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
62152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 
62153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64595      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
64596      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65405      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.09ms 
65407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65408      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314ns 
65409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
67868      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68657      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
68659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68660      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 
68661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
71096      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71883      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
71884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71885      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.5ns 
71885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
74317      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ms 
75127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.9ns 
75128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
77553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78363      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
78364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
78366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
80785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81604      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
81606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140ns 
81607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
84011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84803      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
84805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
84806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
87207      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.29ms 
88050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
88051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
90461      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91296      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.82ms 
91298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
91299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
93700      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94520      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.45ms 
94522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.5ns 
94523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
96917      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
97714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
97714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
100121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
100932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
100933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
103323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.85ms 
104132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
104133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
106530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
107326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
107327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
109719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
110517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
110518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
112911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
113706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
113707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
116115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
116915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
116915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
119323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
120111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
120120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
120121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
120122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
120123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
122518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
123310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
123340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.51ms 
123341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
123341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
123342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
125735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
126524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
126538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
126543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
126544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.2ns 
126545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
128932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.88ms 
129743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 929.61ns 
129745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
132149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.31ms 
132962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.9ns 
132963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
135359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
136164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
136165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
136165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns 
136166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
138555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
139331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
139375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.93ms 
139379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
139380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.4ns 
139381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
141800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
142565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
142567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
142569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
142569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
142570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
144990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
145764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
145769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
145771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
145771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.4ns 
145772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
148196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
148969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
148970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
151384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
152159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
152161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
152161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
152161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
154573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
155337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
155352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
155354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
155354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns 
155354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
157763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
158530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
158537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
158538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
158538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns 
158539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
160961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
161733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
161736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
161739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
161739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
161740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
164146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
164934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
164937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
164938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
164939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130ns 
164939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
167331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
168119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
168122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
168125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
168125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277ns 
168126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
170505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
171295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
171367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.85ms 
171370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
171370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.2ns 
171375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
173766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
174556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
174623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.32ms 
174625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
174625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.8ns 
174626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
177005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
177793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
177796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
177798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
177799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.2ns 
177800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
180185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
180971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
181002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.68ms 
181005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
181005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 465.7ns 
181006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
183398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
184187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
184208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.05ms 
184209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
184209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
184210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
186615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
187408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
187412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.61ns 
187422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
187422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.8ns 
187423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
189853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
190639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
190743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.3ms 
190744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
190745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
190745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
193133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
193919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
193927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
193929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
193929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
193929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
196319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
197108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
197114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
197116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
197116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
197116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
199510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
200294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
200309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.71ms 
200310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
200310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
200311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
202703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
203487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
203498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
203500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
203500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
203501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
205880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
206660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
206664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
206665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
206665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
206666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
209045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
209829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
209833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
209834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
209834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
209835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
212230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
213020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
213047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.83ms 
213048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
213048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
213049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
215454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
216246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
216259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
216260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
216260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
216261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
218662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
219446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
219458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
219459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
219459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
219460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
221841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
222626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
222629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
222631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
222631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
222631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
225019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
225804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
225807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
225809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
225810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.8ns 
225811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
228198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
228964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
228969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
228970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
228970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
228971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
231378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
232143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
232147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.21ns 
232150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
232151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.22ms 
232154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
234558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
235320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
235322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 482.01ns 
235323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
235323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
235324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
237732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
238492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
238495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
238496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
238496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
238497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
240911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
241672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
241675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.6ns 
241677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
241677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 
241678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
244080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
244842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
244876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ms 
244878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
244878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.5ns 
244879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
247279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
248041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
248071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.42ms 
248073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
248073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
248074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
250480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
251241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
251262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.07ms 
251264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
251264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
251264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
253662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
254446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
254475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.35ms 
254476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
254476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
254477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
256861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
257650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
257669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.46ms 
257670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
257670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
257671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
260062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
260847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
260882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.23ms 
260883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
260883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
260884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
263337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
264139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
264140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
264140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
264141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
266516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
267306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
267320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
267321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
267321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
267322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
269699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
270483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
270499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
270500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
270500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
270501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
272877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
273662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
273675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
273676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
273676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
273677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
276055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
276840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
276858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.68ms 
276859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
276859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
276860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
279258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
280047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
280064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
280066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
280066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
280067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
282460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
283274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.32ms 
283276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
283276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.3ns 
283277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
285660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
286446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
286462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
286464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
286464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
286464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
288855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
289647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
289662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
289663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
289663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
289664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
292060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
292847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
292874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.66ms 
292876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
292876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns 
292877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
295271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
296059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
296076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
296077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
296077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
296078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
298462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
299246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
299253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
299254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
299254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
299255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
301642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
302442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
302443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
302443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
302444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
304835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
305627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
305630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
305632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
305632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
305632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
308026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
308814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
308816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.4ns 
308817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
308818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
308818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
311203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
311992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
311994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.31ns 
311996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
311996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
311996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
314389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
315177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
315182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
315184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
315184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
315184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
317576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
318374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
318379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
318381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
318382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.9ns 
318382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
320770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
321544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
321545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
321545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
321546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
323947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
324710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
324713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
324715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
324715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
324715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
327123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
327892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
327894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 445.6ns 
327896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
327896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
327896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
330305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
331068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
331073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
331074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
331074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
331075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
333485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
334248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
334250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.81ns 
334251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
334251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
334252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
336658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
337422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
337424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 502.7ns 
337425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
337425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
337426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
339830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
340595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
340597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 494.2ns 
340598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
340598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
340599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
342988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
343775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
343779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
343780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
343780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
343781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
346167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
346963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
346970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
346971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
346971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
346972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
349361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
350150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
350154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
350155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
350155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
350156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
352534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
353324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
353330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
353331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
353331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
353332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
355710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
356495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
356499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
356500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
356500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
356501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
358888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
359682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
359696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
359699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
359699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.2ns 
359700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
362084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
362872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
362875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
362877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
362877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
362877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
365270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
366062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
366065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
366066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
366067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
366067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
368461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
369252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
369256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
369257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
369257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
369258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
371643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
372429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
372442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
372444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
372444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
372444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
374830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
375615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
375620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 351.3ns 
375621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
375621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
375622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
378006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
378790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
378817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.07ms 
378818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
378818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
378819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
381198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
381984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
381987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
381989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
381989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
381989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
384370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
385156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
385170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.84ms 
385172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
385172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
385173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
387569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
388355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
388369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
388371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
388371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
388372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
390770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
391563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
391580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
391581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
391582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
391582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
393983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
394773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
394776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.7ns 
394778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
394778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.6ns 
394779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
397169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
397958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
397963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
397964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
397964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
397965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
400363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
401156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
401160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
401162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
401162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
401163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
403568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
404338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
404340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 812.41ns 
404342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
404342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
404342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
406749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
407518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
407521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.31ns 
407522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
407522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
407523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
409936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
410707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
410710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
410712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
410712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
410713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
413130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
413900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
413903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
413904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
413904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
413905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
416307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
417076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
417084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
417086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
417086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
417086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
419490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
420260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
420267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
420269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
420269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
420270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
422682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
423459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
423467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
423468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
423468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
423469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
425878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
426658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
426666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
426667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
426667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
426668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
429070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
429847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
429851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
429852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
429852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
429853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
432250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
433027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
433031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
433033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
433033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
433033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
435430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
436205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
436207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.71ns 
436209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
436209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
436209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
438614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
439390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
439393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 915.61ns 
439394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
439394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
439395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
441797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
442574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
442577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.3ns 
442578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
442578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
442578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
444983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
445759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
445767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
445769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
445769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
445769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
448191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
448973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
448976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
448977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
448977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
448978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
451383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
452160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
452165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
452167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
452167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
452167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
454581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
455384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
455386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.11ns 
455388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
455388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
455388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
457773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
458580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
458582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.61ns 
458584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
458584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
458584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
460970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
461769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
461772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
461774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
461774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
461774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
464160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
464959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
464961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.71ns 
464963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
464963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
464963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
467348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
468149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
468152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
468153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
468153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
468154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
470529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
471331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
471333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
471334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
471334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
471335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
473706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
474505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
474509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
474510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
474510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
474511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
476889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
477687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
477690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.81ns 
477691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
477691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
477692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
480093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
480869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
480878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
480879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
480879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
480880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
483280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
484057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
484059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537ns 
484060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
484060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
484061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
486461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
487262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
487268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
487269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
487269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
487270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
489660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
490461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
490463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.51ns 
490465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
490465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
490465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
492854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
493654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
493656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.41ns 
493658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
493658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
493658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
496037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
496836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
496839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
496840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
496841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
496841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
499250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
500027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
500029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939.51ns 
500031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
500031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
500031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
502435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
503241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
503243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
503245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
503245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
503245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
505627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
506431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
506433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 949.61ns 
506435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
506435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
506435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
508818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
509618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
509622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
509624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
509624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
509624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
512015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
512819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
512826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
512827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
512827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
512828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
515232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
516010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
516017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
516019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
516019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
516019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
518439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
519239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
519245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
519246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
519246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
519247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
521650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
522452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
522458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
522459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
522459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
522460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
524833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
525633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
525642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.43ms 
525644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
525644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
525644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
528041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
528819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
528829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
528830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
528830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
528831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
531223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
532022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
532031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
532032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
532033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
532033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
534414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
535215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
535222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
535223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
535223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
535224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
537619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
538397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
538417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.22ms 
538418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
538418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
538419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
540818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
541622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
541643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.26ms 
541644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
541644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
541645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
544034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
544838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
544860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.03ms 
544862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
544863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 
544863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
547252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
548054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
548071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.56ms 
548073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
548073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
548074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
550475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
551276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
551294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
551296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
551296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
551297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
553680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
554481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
554526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.37ms 
554527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
554528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
554528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
556930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
557709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
557713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
557714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
557715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
557715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
560113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
560914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
560918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
560920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
560920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
560920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
563303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
564105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
564108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
564109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
564110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
564111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
566514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
567293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
567305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
567307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
567307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
567307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
569706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
570507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
570513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
570515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
570515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
570515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
572890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
573691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
573694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
573695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
573695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
573696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
576100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
576903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
576913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
576914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
576914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
576915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
579301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
580104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
580117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
580119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
580120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.6ns 
580120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
582522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
583323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
583336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.89ms 
583337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
583337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
583337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
585743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
586546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
586549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847.91ns 
586550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
586550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
586551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
588950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
589735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
589738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
589739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
589739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
589740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
592144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
592945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
592950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
592951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
592951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
592952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
595353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
596131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
596136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
596137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
596137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
596138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
598536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
599338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
599378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.35ms 
599380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
599380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
599381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
601782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
602564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
602584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
602586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
602586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.6ns 
602587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
604987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
605787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
605798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
605799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
605799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
605800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
608191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
608970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
608972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 230.9ns 
608973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
608973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
608974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
611381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
612180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
612256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.88ms 
612258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
612258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
612259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
614656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
615459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
615492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.34ms 
615493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
615493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
615494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
617873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
618672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
618674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.2ns 
618675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
618675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
618676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
621072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
621872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
621873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 195.2ns 
621874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
621875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
621875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
624272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
625052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
625054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 196.4ns 
625055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
625055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
625056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
627451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
628253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
628254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 327ns 
628256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
628256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
628256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
630647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
631449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
631535     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
631542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.65ms 
631544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
631545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.7ns 
631546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
633940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
634743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
634783     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
634787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.71ms 
634789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
634789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
634790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
637197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
638002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
638004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
638034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
638093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
638111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
638122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
638137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
638138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
638140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
638142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
638149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
638149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
638154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
638156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
638380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
638381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
638383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
638384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
638386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
638518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
638519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
638521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
638522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
638524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
638525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
638705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
638707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
638708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
638709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
638711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
638714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
638853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
638855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
638856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
638857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
638858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
638859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
638875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
638876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
638877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
638879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
638880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
638881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
638891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
638892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
638893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
638894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
638894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
638895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
639035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
639036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
639038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
639170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
639171     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)'' 
639173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
639175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
639176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
639177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
639178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
639181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
639186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
639187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
639188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
639189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
639305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
639309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
639310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
639312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
639313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
639314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
639316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
639449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
639451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
639452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
639454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
639455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
639456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
639458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
639459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
639559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
639561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
639654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
639658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
639665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
639667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
639669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
639670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
639670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
639671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
639671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
639681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
639686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
639792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
639795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
639797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
639798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
639799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
639799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
639858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
639864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
639990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
639992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
639993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
639995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
639996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
639997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
640155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
640159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
640161     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)'' 
640164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
640165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
640166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
640167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
640167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
640177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
640183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
640184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
640186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
640291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
640292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
640294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
640295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
640295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
640296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
640417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
640418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
640419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
640421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
640422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
640423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
640423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
640424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
640517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
640519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
640643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
640644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
640644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
640649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
640653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
640659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
640797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
640798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
640799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
640800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
640817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
640917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
644512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
644513     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)'' 
644517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
644519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
644520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
644521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
644522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
644529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
644530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
644531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
644532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
644533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
644623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
644627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
644628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
644629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
644629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
644630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
644631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
644723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
644724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
644725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
644726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
644727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
644727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
644728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
644729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
644805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
644807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
644886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
644890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
644894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
644896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
644897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
644898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
644908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
644994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
644995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
644996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
644997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
645065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
645075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
645076     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)'' 
645077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
645078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
645079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
645079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
645080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
645090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
645091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
645092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
645093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
645094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
645180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
645180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
645182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
645183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
645184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
645272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
645276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
645277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
645278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
645278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
645279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
645280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
645425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
645426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
645427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
645428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
645428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
645429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
645430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
645430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
645431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
645432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
645433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
645434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
645435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
645435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
645436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
645518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
645519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
645525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
645599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
645676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
645678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
645678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
645679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
645680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
645681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
645681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
645682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
645682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
645765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
645771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
645857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
645858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
645859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
645860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
645861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
645861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
645862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
645862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
645867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
645868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
645943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
645949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
645954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
646050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
646051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
646052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
646053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
646054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
646054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
646054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
646055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
646109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
646110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
646111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
646112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
646112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
646118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
646123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
646236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
646319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
646320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
646321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
646321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
646479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
646563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
646563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
649477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
649481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
649482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
649483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
649484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
649594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
649595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
649596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
649597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
649598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
649699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
652435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
655443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
655447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
655448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
655449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
655450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
655559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
655559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
655560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
655561     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)' ...' 
655562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
656651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
656651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
656652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
659126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
659908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
659909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
659909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
659915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
659924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
659926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
659928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
659930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
659938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
659938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
659940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
659949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
659949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
660013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
660060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
660060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
660061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
660061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
660062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
660128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
660128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
660129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
660130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
660130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
660135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
660135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
660135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
660136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
660137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
660137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
660223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
660223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
660223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
660224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
660225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
660225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
660314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
660314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
660314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
660315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
660315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
660316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
660316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
660317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
660317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
660318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
660318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
660318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
660319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
660319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
660319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
660320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
660320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
660320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
660321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
660323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
660362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
660363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
660426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
660427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
660428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
660429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
660430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
660430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
660486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
660488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
660488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
660489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
660490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
660491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
660492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
660538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
660540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
660543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
660601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
660657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
660657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
660658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
663055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
663894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
663910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms