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

198

tests

0

failures

0

ignored

10m46.01s

duration

100%

successful

Tests

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

Standard output

834        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
852        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.81ms 
1044       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1059       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)

1949       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1953       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1957       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1957       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3286       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8242       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.2s 
8305       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8336       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.5ns 
8349       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8349       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
8353       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
11146      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.37ms 
12125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns 
12127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14757      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
14758      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
15631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.31ns 
15633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
18249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19114      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
19117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19117      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
19118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
21602      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms 
22486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 619.01ns 
22489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
24967      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25820      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms 
25823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
25824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
28284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.62ms 
29138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
29139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
31561      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32367      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 783.01ns 
32369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.9ns 
32370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
34785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.61ns 
35592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
35593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
38019      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38835      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.21ns 
38838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 
38840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
41238      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42034      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.2ns 
42037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.3ns 
42038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
44426      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45214      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.31ns 
45217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.9ns 
45219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47604      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
47604      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48428      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.05ms 
48430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
48431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
50818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51673      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.33ms 
51682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.16ms 
51685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54087      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
54088      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55079      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.8ms 
55084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55084      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.61ns 
55086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
57493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58285      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
58288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58288      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.7ns 
58289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
60700      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61494      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
61498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376ns 
61499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
63908      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64758      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.64ms 
64762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
64763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
67171      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms 
67971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
67972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
70373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71178      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms 
71180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
71181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
73589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74397      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.08ms 
74401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.91ns 
74402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
76812      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77612      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
77615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77615      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns 
77616      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
80004      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80818      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.38ms 
80819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns 
80820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
83218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84011      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
84012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
84013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
86399      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87223      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.34ms 
87225      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87225      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
87226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
89612      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.17ms 
90465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.11ns 
90467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
92874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93704      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.45ms 
93706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.8ns 
93707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
96089      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96850      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
96853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96853      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
96854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
99250      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.87ms 
100016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
100017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
102410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
103175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
103176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
105580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
106342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.8ns 
106343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
108738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
109560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.8ns 
109562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
111970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
112735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
112736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
115126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
115881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
115882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
118296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms 
119079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
119081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
121470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.29ms 
122309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 624.51ns 
122319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
124696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms 
125501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 548.11ns 
125503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
127873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
128648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
128666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
128667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
128667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
128668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
131037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
131817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
131835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
131836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
131836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
131837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
134200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
134983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms 
135001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
135002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
137361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.35ms 
138175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
138176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
140541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
141318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
141319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
143676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
144456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
144456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
146820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
147598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
147606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
147607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
147608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
147608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
149974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
150750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
150759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
150761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
150761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 
150762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
153128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
153901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
153920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.13ms 
153921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
153921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
153922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
156281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms 
157070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.3ns 
157072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
159435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
160222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 
160223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
162593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
163381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.9ns 
163382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
165750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
166522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
166527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
166528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
166528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
166529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
168893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
169665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
169740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.94ms 
169742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
169742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299ns 
169744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
172105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
172877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
172963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.21ms 
172965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
172965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
172966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
175326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
176106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.6ns 
176108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
178482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.55ms 
179319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.87ms 
179325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
181690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.08ms 
182495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
182496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
184866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
185640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
185643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
185645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
185645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
185646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
188015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
188791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
188938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.59ms 
188940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
188940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
188941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
191322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
192109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
192110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
194509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.81ms 
195311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
195312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
197677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
198465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
198466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
198466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
198467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
200830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
201606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
201623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.27ms 
201626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
201626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
201626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
203983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
204753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
204756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
204757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
204757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
204758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
207112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
207863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
207867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
207869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
207869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
207869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
210260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms 
211037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
211038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
213434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
214202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
214203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
216582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms 
217346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
217347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
219719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
220467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
220471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
220472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
220472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
220473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
222856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
223603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
223608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
223610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
223610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.6ns 
223611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
225990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
226738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
226743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
226744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
226744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
226745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
229125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
229877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
229880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
229881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
229881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
229882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
232267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
233016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
233019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.31ns 
233021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
233021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.2ns 
233022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
235383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
236163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
236167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
236168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
236168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
236169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
238536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
239313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
239316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.61ns 
239317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
239317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
239318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
241683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
242454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
242500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.09ms 
242503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
242503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns 
242504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
244867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
245638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
245672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.61ms 
245673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
245673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
245674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
248052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
248823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
248852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.38ms 
248853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
248853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
248854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
251221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
251994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
252036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.76ms 
252038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
252038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
252039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
254396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
255169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
255197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.21ms 
255198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
255198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
255199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
257555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
258330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
258377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.68ms 
258379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
258379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
258380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
260741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
261513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
261541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
261542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
261542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
261543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
263898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
264680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
264699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.47ms 
264700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
264701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
264701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
267062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
267837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
267863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.59ms 
267866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
267866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns 
267867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
270223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
270997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
271017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
271018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
271018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
271019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
273374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
274148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
274175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.46ms 
274176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
274176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
274177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
276537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
277312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
277337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.19ms 
277338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
277338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
277339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
279701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
280476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
280500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.71ms 
280502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
280502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
280503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
282859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
283635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
283660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.96ms 
283661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
283661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
283662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
286029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
286802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
286823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.03ms 
286824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
286824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
286825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
289184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
289955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
289980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.73ms 
289981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
289981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
289982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
292343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
293119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
293143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms 
293145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
293145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
293145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
295540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
296313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
296321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
296322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
296322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
296323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
298684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
299458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
299476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.44ms 
299478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
299478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
299479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
301840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
302613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
302617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
302618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
302618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
302619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
304978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
305749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
305751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.61ns 
305752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
305752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
305753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
308103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
308874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
308877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.11ns 
308878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
308878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
308879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
311248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
312019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
312027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
312029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
312029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.1ns 
312030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
314391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
315168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
315175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
315177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
315177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.1ns 
315178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
317535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
318311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
318323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
318325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
318325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
318325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
320682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
321432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
321436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
321438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
321438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
321438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
323809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
324557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
324559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.21ns 
324561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
324561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.1ns 
324562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
326929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
327679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
327687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
327689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
327689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 
327690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
330067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
330815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
330817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.41ns 
330819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
330819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
330819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
333201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
333950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
333952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.51ns 
333953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
333953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
333954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
336326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
337073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
337075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.21ns 
337076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
337076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
337077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
339452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
340202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
340206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
340207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
340207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
340208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
342587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
343341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
343350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
343352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
343352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
343352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
345705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
346477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
346481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
346482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
346483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
346483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
348841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
349613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
349620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
349621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
349621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
349622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
351975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
352747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
352751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
352753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
352753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
352753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
355114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
355886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
355902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
355903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
355903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
355904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
358264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
359043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
359047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
359050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
359050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192ns 
359051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
361406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
362181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
362184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
362185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
362185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
362186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
364536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
365307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
365311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
365312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
365312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
365313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
367660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
368431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
368450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms 
368452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
368452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
368452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
370809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
371583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
371588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.31ns 
371591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
371591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.1ns 
371592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
373937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
374703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
374742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.13ms 
374743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
374743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
374744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
377104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
377877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
377881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
377882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
377882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
377883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
380232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
381003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
381025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.74ms 
381026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
381026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
381027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
383380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
384150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
384171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.99ms 
384172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
384172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
384173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
386541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
387316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
387340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.05ms 
387341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
387341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
387342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
389706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
390481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
390484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.01ns 
390485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
390485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
390486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
392851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
393624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
393630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
393631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
393631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
393632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
395989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
396770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
396774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
396776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
396776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
396777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
399156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
399931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
399934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.11ns 
399935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
399935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.49ns 
399936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
402291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
403066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
403069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.91ns 
403071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
403071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns 
403071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
405428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
406205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
406209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
406210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
406210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
406211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
408568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
409347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
409350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
409351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
409351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
409352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
411708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
412485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
412494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
412497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
412497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
412498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
414860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
415639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
415651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms 
415652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
415652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
415653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
418003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
418786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
418797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.83ms 
418798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
418798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
418799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
421150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
421933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
421945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ms 
421946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
421946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
421947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
424299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
425082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
425087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
425088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
425088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
425089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
427439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
428217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
428223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
428224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
428224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
428225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
430575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
431354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
431356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.71ns 
431357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
431357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
431358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
433719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
434497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
434500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
434501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
434501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
434502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
436853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
437632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
437634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.51ns 
437637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
437637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 
437638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
440004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
440783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
440793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
440795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
440795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
440795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
443152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
443931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
443935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
443936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
443936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
443937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
446287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
447065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
447072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
447074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
447074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 
447075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
449432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
450213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
450215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.61ns 
450216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
450216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
450217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
452562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
453341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
453343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.51ns 
453344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
453344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
453345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
455689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
456467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
456471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
456472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
456472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
456473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
458819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
459601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
459604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
459606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
459606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns 
459607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
461961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
462741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
462744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
462745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
462745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
462746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
465119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
465878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
465880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
465882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
465882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
465882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
468255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
469012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
469017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
469018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
469018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
469019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
471390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
472146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
472149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
472150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
472150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
472151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
474518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
475298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
475309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
475311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
475311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
475312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
477661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
478440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
478442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.61ns 
478443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
478443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
478444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
480792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
481577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
481584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
481585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
481585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
481586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
483931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
484710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
484712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 908.51ns 
484714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
484714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
484714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
487060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
487840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
487842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.51ns 
487844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
487844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
487844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
490221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
490978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
490983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
490984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
490984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
490985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
493374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
494154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
494157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
494159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
494160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 
494160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
496518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
497297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
497301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
497303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
497303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
497304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
499659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
500442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
500446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
500448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
500448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
500449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
502802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
503585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
503589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
503591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
503592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
503592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
505961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
506718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
506732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
506733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
506733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
506734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
509099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
509878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
509893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
509895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
509895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
509896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
512246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
513033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
513043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
513044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
513044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
513045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
515391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
516173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
516186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.68ms 
516187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
516187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
516188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
518562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
519319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
519345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.02ms 
519346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
519346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
519347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
521718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
522499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
522524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
522526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
522526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
522526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
524875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
525654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
525677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
525678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
525678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
525679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
528020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
528800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
528814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
528815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
528816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
528816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
531190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
531969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
531999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.38ms 
532001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
532001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
532002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
534355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
535136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
535183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.65ms 
535184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
535184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
535185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
537538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
538320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
538357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.06ms 
538359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
538359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
538360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
540724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
541505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
541546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.98ms 
541548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
541548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
541549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
543897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
544679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
544722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.21ms 
544724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
544724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
544725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
547093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
547850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
547967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.05ms 
547968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
547969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
547969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
550343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
551125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
551133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
551134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
551135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
551135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
553477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
554256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
554264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
554265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
554265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
554266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
556631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
557390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
557395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
557396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
557396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
557397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
559764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
560545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
560563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.09ms 
560565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
560565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
560565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
562906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
563687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
563700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms 
563701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
563701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
563702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
566073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
566852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
566855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
566856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
566856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
566857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
569204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
569986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
570003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.96ms 
570004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
570004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
570005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
572380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
573167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
573183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
573185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
573185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
573186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
575533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
576314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
576333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms 
576334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
576334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
576335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
578703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
579462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
579465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
579466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
579466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
579467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
581834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
582614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
582617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
582618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
582618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
582619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
584970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
585754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
585761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
585762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
585762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
585762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
588146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
588926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
588932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
588933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
588933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
588934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
591284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
592066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
592137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.9ms 
592138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
592138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
592139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
594525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
595305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
595331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.17ms 
595332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
595332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
595333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
597704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
598463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
598485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.27ms 
598486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
598486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
598487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
600854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
601641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
601643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.6ns 
601645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
601645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
601646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
604026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
604786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
605019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.64ms 
605021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
605021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
605022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
607376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
608160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
608209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.27ms 
608211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
608211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
608211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
610590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
611372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
611374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 374ns 
611378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
611378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234ns 
611379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
613736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
614518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
614520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.11ns 
614521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
614521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
614522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
616883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
617661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
617663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.11ns 
617664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
617664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
617665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
620033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
620793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
620795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.51ns 
620796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
620796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
620797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
623160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
623941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
624051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.17ms 
624053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
624053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns 
624054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
626442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
627224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
627276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.43ms 
627277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
627277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
627279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
629654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
630436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
630438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
630467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
630513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
630535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
630543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
630551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
630553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
630554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
630557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
630560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
630562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
630566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
630567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
630778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
630779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
630780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
630781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
630782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
630902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
630903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
630906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
630909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
630910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
630911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
631058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
631060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
631061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
631062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
631063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
631067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
631169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
631171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
631172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
631173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
631174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
631175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
631181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
631182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
631183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
631185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
631186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
631187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
631193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
631195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
631196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
631197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
631198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
631199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
631311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
631312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
631314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
631413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
631414     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)'' 
631417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
631418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
631419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
631421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
631422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
631424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
631428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
631430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
631431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
631431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
631432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
631557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
631560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
631562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
631563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
631564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
631565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
631567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
631667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
631669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
631670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
631671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
631671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
631672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
631673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
631675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
631751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
631752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
631871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
631874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
631879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
631880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
631881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
631882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
631884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
631885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
631885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
631887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
631893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
631897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
631981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
631983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
631984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
631986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
631988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
631988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
631989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
631990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
632037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
632041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
632117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
632119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
632120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
632122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
632123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
632124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
632227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
632230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
632232     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)'' 
632234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
632235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
632236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
632237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
632237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
632244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
632249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
632251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
632251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
632328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
632330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
632331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
632332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
632332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
632333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
632420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
632422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
632423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
632425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
632425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
632426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
632427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
632428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
632518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
632519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
632580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
632580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
632581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
632584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
632587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
632591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
632689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
632690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
632691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
632692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
632699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
632767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
635954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
635955     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)'' 
635960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
635961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
635962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
635963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
635965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
635972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
635973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
635975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
635976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
635978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
636060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
636063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
636064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
636065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
636065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
636066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
636067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
636193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
636194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
636195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
636196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
636197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
636197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
636198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
636199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
636265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
636266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
636328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
636332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
636335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
636336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
636337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
636338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
636346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
636414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
636415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
636416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
636417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
636480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
636487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
636488     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)'' 
636490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
636491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
636492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
636492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
636493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
636502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
636503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
636504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
636505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
636506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
636581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
636583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
636584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
636585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
636585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
636663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
636667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
636668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
636669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
636669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
636670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
636670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
636755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
636756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
636757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
636758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
636759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
636760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
636760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
636761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
636762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
636763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
636764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
636765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
636765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
636766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
636767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
636842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
636843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
636849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
636916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
636985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
636986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
636987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
636987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
636988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
636989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
636989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
636989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
636990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
637064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
637069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
637146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
637147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
637148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
637149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
637149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
637150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
637150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
637151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
637155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
637156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
637224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
637228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
637233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
637318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
637319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
637320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
637321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
637321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
637321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
637321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
637322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
637369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
637370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
637370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
637371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
637372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
637376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
637381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
637482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
637559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
637560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
637560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
637561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
637708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
637784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
637784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
640499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
640504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
640505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
640506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
640506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
640605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
640607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
640608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
640608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
640609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
640699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
643336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
646161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
646166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
646167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
646168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
646168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
646267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
646269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
646270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
646271     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)' ...' 
646272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
647305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
647305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.9ns 
647306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
649749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
650509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
650510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
650510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
650516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
650527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
650529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
650531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
650531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
650534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
650536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
650538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
650540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
650541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
650548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
650550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
650550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
650639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
650640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
650641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
650641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
650642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
650701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
650701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
650703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
650703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
650704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
650706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
650707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
650707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
650708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
650709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
650709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
650780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
650781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
650781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
650782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
650783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
650784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
650857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
650857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
650858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
650859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
650859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
650859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
650860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
650860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
650862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
650862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
650863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
650863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
650864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
650864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
650866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
650899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
650900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
650952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
650953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
650954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
650955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
650956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
650956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
651003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
651005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
651006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
651007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
651008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
651009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
651009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
651058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
651060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
651063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
651125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
651182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
651182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
651183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
653548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
654346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
654375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.76ms