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

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

tests
0

failures
0

ignored
11m6.18s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.216s passed
powPositiveConcrete data()[101] 3.213s passed
powGeq1Concrete data()[102] 3.198s passed
pow2InIntLower data()[103] 3.210s passed
pow2InIntUpper data()[104] 3.380s passed
logSelfConcrete data()[105] 3.319s passed
log1Concrete data()[106] 3.228s passed
logProduct data()[107] 3.213s passed
logTimesBaseConcrete data()[108] 3.211s passed
logProdIdentity data()[109] 3.219s passed
moduloByteIsInByte data()[10] 3.294s passed
logProdIdentityConcrete data()[110] 3.212s passed
logPowIdentity data()[111] 3.218s passed
logPowIdentityConcrete data()[112] 3.234s passed
logPositive data()[113] 3.265s passed
logPositiveConcrete data()[114] 3.219s passed
logMono data()[115] 3.254s passed
logMonoConcrete data()[116] 3.223s passed
powLogLess data()[117] 3.239s passed
powLogMore2 data()[118] 3.238s passed
logLessThanPow data()[119] 3.257s passed
moduloCharIsInChar data()[11] 3.273s passed
logLessThanPowConcrete data()[120] 3.221s passed
logSqueeze data()[121] 3.227s passed
ifthenelse_equals data()[122] 3.220s passed
ifthenelse_equals_1 data()[123] 3.221s passed
ifthenelse_equals_2 data()[124] 3.220s passed
disjointWithSingleton1 data()[125] 3.227s passed
disjointWithSingleton2 data()[126] 3.221s passed
disjointArrayRanges data()[127] 3.227s passed
disjointArrayRangeAllFields1 data()[128] 3.226s passed
disjointArrayRangeAllFields2 data()[129] 3.240s passed
div_unique1 data()[12] 3.360s passed
seqSelfDefinition data()[130] 3.230s passed
seqOutsideValue data()[131] 3.227s passed
castedGetAny data()[132] 3.239s passed
seqGetAlphaCast data()[133] 3.232s passed
getOfSeqSingleton data()[134] 3.246s passed
getOfSeqSingletonConcrete data()[135] 3.223s passed
getOfSeqConcat data()[136] 3.224s passed
getOfSeqSub data()[137] 3.242s passed
getOfSeqReverse data()[138] 3.237s passed
lenOfSeqEmpty data()[139] 3.215s passed
div_unique2 data()[13] 3.328s passed
lenOfSeqSingleton data()[140] 3.216s passed
lenOfSeqConcat data()[141] 3.241s passed
lenOfSeqSub data()[142] 3.240s passed
lenOfSeqReverse data()[143] 3.244s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.247s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.234s passed
getOfSeqSingletonEQ data()[146] 3.236s passed
getOfSeqConcatEQ data()[147] 3.223s passed
getOfSeqSubEQ data()[148] 3.239s passed
getOfSeqReverseEQ data()[149] 3.227s passed
div_exists data()[14] 3.429s passed
lenOfSeqEmptyEQ data()[150] 3.248s passed
lenOfSeqSingletonEQ data()[151] 3.219s passed
lenOfSeqConcatEQ data()[152] 3.235s passed
lenOfSeqSubEQ data()[153] 3.236s passed
lenOfSeqReverseEQ data()[154] 3.249s passed
getOfSeqDefEQ data()[155] 3.233s passed
lenOfSeqDefEQ data()[156] 3.253s passed
seqConcatWithSeqEmpty1 data()[157] 3.238s passed
seqConcatWithSeqEmpty2 data()[158] 3.246s passed
seqReverseOfSeqEmpty data()[159] 3.248s passed
div_one data()[15] 3.300s passed
subSeqComplete data()[160] 3.245s passed
subSeqTailR data()[161] 3.268s passed
subSeqTailL data()[162] 3.265s passed
subSeqTailEQR data()[163] 3.264s passed
subSeqTailEQL data()[164] 3.239s passed
seqDef_split data()[165] 3.273s passed
seqDef_induction_upper data()[166] 3.286s passed
seqDef_induction_upper_concrete data()[167] 3.276s passed
seqDef_induction_lower data()[168] 3.288s passed
seqDef_induction_lower_concrete data()[169] 3.282s passed
jdiv_one data()[16] 3.277s passed
seqDef_split_in_three data()[170] 3.365s passed
seqDef_empty data()[171] 3.271s passed
seqDef_one_summand data()[172] 3.233s passed
seqDef_lower_equals_upper data()[173] 3.241s passed
seqDefOfSeq data()[174] 3.257s passed
seqSelfDefinitionEQ2 data()[175] 3.243s passed
indexOfSeqSingleton data()[176] 3.231s passed
indexOfSeqConcatFirst data()[177] 3.241s passed
indexOfSeqConcatSecond data()[178] 3.240s passed
indexOfSeqSub data()[179] 3.264s passed
div_zero data()[17] 3.342s passed
lenOfArray2seq data()[180] 3.305s passed
getAnyOfArray2seq data()[181] 3.216s passed
getOfArray2seq data()[182] 3.220s passed
getAnyOfNPermInv data()[183] 3.231s passed
seqNPermRange data()[184] 3.323s passed
seqPermTrans data()[185] 3.298s passed
seqPermRefl data()[186] 3.276s passed
seqPermSplit data()[187] 3.222s passed
seqNPermRight data()[188] 3.446s passed
seqPermFromSwap data()[189] 3.308s passed
divResZero1 data()[18] 3.282s passed
seqPermTransAlt0 data()[190] 3.238s passed
seqPermTransAlt1 data()[191] 3.236s passed
seqPermTransAlt2 data()[192] 3.264s passed
seqPermTransAlt3 data()[193] 3.249s passed
seqPermForall data()[194] 3.346s passed
seqPermExists data()[195] 3.284s passed
schiffl_lemma_2 data()[196] 22.082s passed
schiffl_thm_1 data()[197] 4.052s passed
eqSameSeq data()[198] 3.265s passed
divResZero2 data()[19] 3.256s passed
eqTermCut data()[1] 3.825s passed
divResOne1 data()[20] 3.290s passed
divResOne2 data()[21] 3.298s passed
div_cancel1 data()[22] 3.246s passed
div_cancel2 data()[23] 3.282s passed
divAddMultDenom data()[24] 3.281s passed
divMinus data()[25] 3.284s passed
divMinusDenom data()[26] 3.290s passed
divLeastDPos data()[27] 3.249s passed
divLeastDNeg data()[28] 3.236s passed
divGreatestDPos data()[29] 3.252s passed
equivAllRight data()[2] 3.586s passed
divGreatestDNeg data()[30] 3.241s passed
divIncreasingPos data()[31] 3.256s passed
divIncreasingNeg data()[32] 3.257s passed
jdiv_zero data()[33] 3.236s passed
jdivPulloutMinusNum data()[34] 3.248s passed
jdivPulloutMinusDenom data()[35] 3.272s passed
jdiv_uniquePosPos data()[36] 3.244s passed
jdiv_uniquePosNeg data()[37] 3.247s passed
jdiv_uniqueNegPos data()[38] 3.233s passed
jdiv_uniqueNegNeg data()[39] 3.345s passed
irrflConcrete1 data()[3] 3.472s passed
jdivMultDenom1 data()[40] 3.414s passed
jdivMultDenom2 data()[41] 3.360s passed
mod_geZero data()[42] 3.361s passed
mod_lessDenom data()[43] 3.270s passed
jmod_NumPos data()[44] 3.371s passed
jmod_NumNeg data()[45] 3.348s passed
jmod_geZero data()[46] 3.239s passed
jmodNumZero data()[47] 3.240s passed
jmod_pulloutminusNum data()[48] 3.252s passed
jmod_pulloutminusDenom data()[49] 3.237s passed
irrflConcrete2 data()[4] 3.458s passed
jmodUnique1 data()[50] 3.282s passed
jmodUnique2 data()[51] 3.313s passed
intDivRem data()[52] 3.228s passed
jmodjmod data()[53] 3.247s passed
jmodDivisible data()[54] 3.258s passed
jmodDivisibleRep data()[55] 3.331s passed
jdivAddMultDenom data()[56] 3.374s passed
jmodAltZero data()[57] 3.228s passed
jmodAddMultDenomZero data()[58] 3.237s passed
polyDiv_zero data()[59] 3.235s passed
cancel_gtPos data()[5] 3.391s passed
polyMod_ltdivDenom data()[60] 3.207s passed
bsum_empty data()[61] 3.200s passed
bsum_induction_upper data()[62] 3.214s passed
bsum_induction_lower data()[63] 3.227s passed
bsum_num_of_bounds data()[64] 3.247s passed
bsum_num_of_bounds2 data()[65] 3.231s passed
bsum_induction_upper2 data()[66] 3.219s passed
bsum_induction_upper_concrete data()[67] 3.224s passed
bsum_induction_upper_concrete_2 data()[68] 3.225s passed
bsum_induction_upper2_concrete data()[69] 3.201s passed
cancel_gtNeg data()[6] 3.361s passed
bsum_induction_lower_concrete data()[70] 3.213s passed
bsum_induction_lower2 data()[71] 3.211s passed
bsum_induction_lower2_concrete data()[72] 3.190s passed
bsum_positive data()[73] 3.268s passed
bsum_upper_bound data()[74] 3.278s passed
bsum_lower_bound data()[75] 3.222s passed
bsum_positive_lower_bound_element data()[76] 3.347s passed
bsum_sub_same_index data()[77] 3.279s passed
bsum_less_same_index data()[78] 3.257s passed
bsum_equal_except_one_index data()[79] 3.254s passed
moduloIntIsInInt data()[7] 3.335s passed
bsum_num_of_is_max data()[80] 3.250s passed
bsum_num_of_is_max2 data()[81] 3.261s passed
bsum_num_of_is_max3 data()[82] 3.239s passed
bsum_num_of_is_max4 data()[83] 3.256s passed
bsum_num_of_lt_max data()[84] 3.269s passed
bsum_num_of_lt_max2 data()[85] 3.241s passed
bsum_num_of_lt_max3 data()[86] 3.258s passed
bsum_num_of_lt_max4 data()[87] 3.244s passed
bsum_num_of_gt0 data()[88] 3.241s passed
bsum_num_of_gt0_alt data()[89] 3.254s passed
moduloLongIsInLong data()[8] 3.309s passed
bsum_add_concrete data()[90] 3.248s passed
bprod_all_positive data()[91] 3.235s passed
bprod_split data()[92] 3.240s passed
powConcrete0 data()[93] 3.255s passed
powConcrete1 data()[94] 3.236s passed
powSplitFactor data()[95] 3.264s passed
powAdd data()[96] 3.256s passed
powMono data()[97] 3.259s passed
powMonoConcrete data()[98] 3.234s passed
powMonoConcreteRight data()[99] 3.215s passed
moduloShortIsInShort data()[9] 3.308s passed

Standard output

558        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
588        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 16.17ms 
814        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833        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)

1765       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1767       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3366       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8643       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.83s 
8724       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8760       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.2ns 
8775       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8778       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.12ms 
8785       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
11645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12592      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 
12606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.8ns 
12608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
15304      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
16195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1ms 
16198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18788      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
18788      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
19671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.6ns 
19673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22221      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
22221      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.37ms 
23128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 861.1ns 
23131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25644      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
25645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26516      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.42ms 
26520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 656.7ns 
26522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
29028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29879      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.64ms 
29881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
29882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
32394      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33214      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.8ns 
33216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
33217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36523      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.3ns 
36524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
36525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
38998      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39830      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594ns 
39833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 691.6ns 
39836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
42293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43125      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617ns 
43127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 
43128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
45590      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46396      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46398      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.2ns 
46400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
46401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
48879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.14ms 
49762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.6ns 
49763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
52245      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53087      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.28ms 
53089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
53090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55539      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
55540      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.99ms 
56518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56518      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 
56519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
59001      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
59818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.8ns 
59819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
62274      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63093      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
63096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.1ns 
63098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65585      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
65585      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66436      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.96ms 
66437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
66438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
68902      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
69720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
69721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
72178      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
72976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72976      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
72977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
75426      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
76266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.3ns 
76268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78750      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
78750      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79562      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.79ms 
79563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
79564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
82003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82809      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.42ms 
82810      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82810      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
82811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
85284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86090      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
86092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.2ns 
86093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
88530      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89371      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.92ms 
89373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.6ns 
89375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
91822      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92655      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.94ms 
92658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.6ns 
92659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
95101      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95945      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.23ms 
95947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
95947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
98392      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99195      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
99196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
99197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
101641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
102432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
102433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
104878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
105684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
105684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
108124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
108925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
108926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
111365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.24ms 
112184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.2ns 
112186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
114635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
115438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
115439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
117877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
118675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.2ns 
118676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
121108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
121929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 582.7ns 
121932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
124354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.8ms 
125201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.7ns 
125202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
127633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
128444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
128445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
130879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms 
131690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.7ns 
131691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
134110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
134924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
134925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
137371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
138269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
138270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
140815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.42ms 
141683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
141683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
144212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
145039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
145042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.89ns 
145043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
145043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
145044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
147586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
148398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
148402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
148403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
148404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
148404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
150847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
151674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.1ns 
151675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
154208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
155035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
155043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
155045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
155045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
155045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
157564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
158359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
158391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.58ms 
158393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
158393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264ns 
158394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
160830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
161622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
161630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
161631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
161631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
161632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
164052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
164871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
164873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 
164874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
167323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
168114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
168118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
168125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
168125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.4ns 
168126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
170564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
171355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
171359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
171375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
171375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.8ns 
171379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
173798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
174590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
174656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.34ms 
174657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
174657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
174658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
177089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.88ms 
177969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
177970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
180403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
181194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
181197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
181198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
181198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
181199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
183637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
184409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
184443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.76ms 
184445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
184445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.8ns 
184445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
186881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
187672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
187702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.22ms 
187703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
187703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
187704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
190231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
191029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
191032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
191034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
191034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.6ns 
191035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
193464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
194236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
194406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 159.86ms 
194409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
194409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
194410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
196827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
197623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
197634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
197635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
197635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
197636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
200074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
200871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
200872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
200872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
200873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
203303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
204091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
204106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
204107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
204108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
204108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
206512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
207299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
207313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.65ms 
207315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
207315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
207315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
209726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
210510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
210513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
210515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
210515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
210515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
212933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
213727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
213729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
213729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
213729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
216143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
216954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms 
216955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
216956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
216956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
219396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
220187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
220202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
220203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
220203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
220204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
222628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
223417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
223432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
223434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
223434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 
223435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
225848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
226648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
226651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
226652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
226652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
226653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
229074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
229875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
229877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
229877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 
229878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
232308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
233096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
233101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
233102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
233102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
233103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
235511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
236299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
236301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
236303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
236303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
236303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
238725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
239512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
239515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.5ns 
239516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
239516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
239516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
241933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
242725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
242726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
242726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
242727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
245126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995ns 
245917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
245918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
248337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
249130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
249183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.81ms 
249185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
249186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns 
249187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
251632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
252422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
252461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.39ms 
252462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
252462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
252463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
254882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
255653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
255683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.66ms 
255685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
255685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
255685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
258193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
259030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.15ms 
259032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
259033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.3ns 
259034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
261485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
262280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
262309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.03ms 
262311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
262311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
262312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
264735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
265513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
265565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.77ms 
265567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
265567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
265568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
268007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
268795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
268821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.13ms 
268822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
268822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
268823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
271261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
272051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
272070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ms 
272072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
272072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
272072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
274508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
275306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
275331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.93ms 
275332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
275332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
275333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
277757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
278551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
278570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms 
278571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
278572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
278572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
281006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
281798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
281827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.96ms 
281828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
281828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
281829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
284273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
285070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
285095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
285097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
285097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
285098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
287520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
288311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
288337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
288338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
288338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
288339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
290776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
291569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
291594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.78ms 
291596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
291596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
291596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
294027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
294818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
294839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.52ms 
294840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
294840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
294841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
297262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
298055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
298080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
298081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
298081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
298082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
300518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
301308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
301333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
301335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
301335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
301335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
303776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
304573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
304581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
304582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
304582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
304583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
307025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
307799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
307817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.36ms 
307818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
307818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
307819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
310259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
311053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
311057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
311058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
311058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
311059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
313513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
314309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
314311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.7ns 
314312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
314313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
314313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
316768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
317545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
317547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.5ns 
317549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
317549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.9ns 
317550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
320002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
320798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
320810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
320814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
320814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.8ns 
320816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
323268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
324062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
324068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
324069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
324069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
324070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
326520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
327316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
327327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
327329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
327329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
327329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
329757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
330558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
330562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
330563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
330563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
330563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
332985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
333774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
333776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 509.1ns 
333777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
333777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
333778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
336199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
336987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
336992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
336993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
336994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
339415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
340203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
340205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.7ns 
340206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
340206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
340207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
342607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
343401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
343403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551.4ns 
343404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
343404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
343405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
345818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
346611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
346613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 961.69ns 
346614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
346614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
346615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
349158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
349990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
349994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
349995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
349995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
349996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
352511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
353303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
353312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
353313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
353313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
353314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
355744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
356536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
356541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
356542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
356542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
356543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
358975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
359746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
359753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
359754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
359755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
359755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
362171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
362961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
362965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
362966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
362966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
362966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
365380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
366168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
366183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
366184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
366184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
366185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
368602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
369392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
369395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
369396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
369396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
369397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
371815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
372610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
372613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
372614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
372614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
372615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
375039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
375843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
375847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
375848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
375848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
375849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
378303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
379095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
379112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
379113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
379113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
379114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
381537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
382327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
382331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.7ns 
382333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
382333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
382333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
384758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
385547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
385586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.63ms 
385587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
385587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
385588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
388013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
388805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
388808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
388809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
388809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
388810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
391238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
392027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
392048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.52ms 
392049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
392049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
392050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
394475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
395265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
395286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ms 
395294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
395294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
395295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
397728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
398518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
398543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.47ms 
398544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
398544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
398545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
400967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
401760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
401763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.1ns 
401765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
401765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191ns 
401766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
404194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
404985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
404990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
404991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
404991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
404992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
407417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
408207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
408210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
408212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
408212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
408212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
410636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
411429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
411431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820.1ns 
411432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
411433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
411433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
413853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
414649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
414651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.1ns 
414652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
414652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
414653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
417079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
417876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
417879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
417880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
417880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
417880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
420302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
421097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
421100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
421101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
421101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
421102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
423523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
424317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
424326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.85ms 
424327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
424327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
424328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
426747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
427540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
427552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
427553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
427553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
427554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
429985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
430781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
430792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
430793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
430793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
430794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
433214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
434011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
434023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
434024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
434024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
434024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
436445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
437245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
437249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
437250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
437250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
437251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
439681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
440483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
440488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
440489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
440489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
440490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
442921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
443719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
443721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.9ns 
443722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
443722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
443723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
446165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
446964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
446966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
446967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
446968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
446968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
449390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
450187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
450189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712ns 
450190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
450190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
450191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
452606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
453404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
453414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
453415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
453415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
453416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
455848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
456649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
456655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
456656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
456656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
456658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
459090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
459886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
459892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
459894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
459894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
459894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
462308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
463106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
463108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.3ns 
463109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
463109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
463110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
465524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
466321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
466323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.5ns 
466324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
466324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
466325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
468762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
469561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
469565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
469566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
469566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
469567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
472003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
472801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
472804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
472805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
472805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
472806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
475245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
476046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
476049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
476050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
476050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
476050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
478490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
479293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
479296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
479297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
479297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
479298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
481723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
482522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
482529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
482530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
482530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
482531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
484965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
485762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
485765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
485766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
485767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
485767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
488183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
488978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
488989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
488990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
488990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
488990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
491427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
492225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
492227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.6ns 
492228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
492228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
492229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
494646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
495447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
495454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
495455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
495455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
495456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
497885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
498700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
498703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859ns 
498704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
498704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
498704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
501123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
501919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
501921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.2ns 
501922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
501922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
501923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
504353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
505152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
505157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
505158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
505158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.5ns 
505159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
507589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
508389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
508392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
508394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
508394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
508395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
510839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
511638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
511641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
511642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
511642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
511643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
514071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
514871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
514874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
514875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
514875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
514876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
517323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
518123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
518128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
518129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
518129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
518129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
520553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
521351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
521365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
521367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
521367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
521367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
523799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
524596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
524612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.29ms 
524613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
524613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
524614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
527052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
527849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
527859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
527860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
527860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
527861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
530296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
531094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
531105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
531106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
531106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
531106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
533548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
534347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
534373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.73ms 
534374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
534374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
534375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
536814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
537612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
537638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.21ms 
537639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
537639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
537639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
540077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
540877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
540901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.93ms 
540902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
540902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
540903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
543328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
544126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
544141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
544142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
544142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
544143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
546582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
547381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
547413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.74ms 
547414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
547414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
547415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
549852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
550652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
550699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.65ms 
550700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
550700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
550701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
553138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
553938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
553975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.35ms 
553977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
553977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
553977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
556418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
557222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
557264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.24ms 
557265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
557265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
557266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
559682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
560501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
560545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.75ms 
560546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
560546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
560547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
562973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
563790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
563910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.47ms 
563911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
563911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
563912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
566350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
567170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
567181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ms 
567182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
567182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
567183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
569606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
570407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
570414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
570416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
570416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
570416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
572852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
573650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
573655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
573656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
573656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
573657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
576096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
576895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
576913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
576914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
576914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
576915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
579347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
580145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
580155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms 
580157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
580157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
580157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
582586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
583383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
583386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
583387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
583387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
583388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
585815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
586611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
586628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.52ms 
586629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
586629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
586629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
589056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
589852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
589868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
589869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
589869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
589870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
592316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
593112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
593131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.27ms 
593132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
593132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
593133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
595601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
596433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
596437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
596438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
596438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
596438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
598859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
599649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
599653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
599654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
599654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
599655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
602070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
602866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
602872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
602873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
602873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
602874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
605292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
606095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
606104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
606105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
606105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
606106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
608555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
609356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
609426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.49ms 
609428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
609428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
609428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
611886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
612694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
612723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.38ms 
612726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
612726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214ns 
612727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
615177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
615978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
616000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.86ms 
616001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
616001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
616002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
618421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
619220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
619222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 274.7ns 
619223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
619224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166ns 
619225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
621668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
622467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
622668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.16ms 
622670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
622670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.4ns 
622671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
625125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
625927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
625977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.22ms 
625978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
625978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
625978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
628413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
629213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
629215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 343.4ns 
629216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
629216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
629217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
631652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
632449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
632451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 347.9ns 
632452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
632452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
632453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
634910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
635713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
635714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 340.4ns 
635716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
635716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
635716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
638142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
638962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
638964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 454ns 
638965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
638965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
638965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
641388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
642207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
642296     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
642309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.05ms 
642311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
642311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.3ns 
642312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
644742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
645542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
645593     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
645594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.52ms 
645595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
645595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
645596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
648035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
648845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
648847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
648870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
648909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
648925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
648928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
648934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
648937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
648937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
648939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
648942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
648943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
648945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
648946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
649163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
649165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
649167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
649169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
649170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
649346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
649347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
649350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
649353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
649354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
649357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
649533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
649535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
649538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
649541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
649654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
649656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
649657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
649658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
649660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
649660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
649674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
649675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
649676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
649687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
649690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
649694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
649702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
649703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
649704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
649705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
649705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
649707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
649841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
649842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
649843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
649974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
649976     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)'' 
649978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
649979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
649980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
649981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
649981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
649982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
649985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
649987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
649988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
649989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
649989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
650105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
650108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
650110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
650111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
650111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
650112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
650113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
650244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
650245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
650246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
650248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
650248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
650249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
650250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
650251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
650355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
650357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
650455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
650459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
650463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
650465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
650465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
650467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
650467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
650468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
650468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
650469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
650477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
650481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
650573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
650574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
650575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
650577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
650577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
650578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
650578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
650579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
650629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
650634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
650726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
650728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
650730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
650732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
650733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
650734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
650847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
650851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
650852     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)'' 
650853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
650854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
650855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
650864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
650865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
650866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
650867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
650949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
650951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
650951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
650952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
650953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
650954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
651046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
651048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
651049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
651050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
651051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
651052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
651052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
651053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
651129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
651131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
651198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
651199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
651200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
651204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
651207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
651211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
651325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
651327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
651328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
651330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
651340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
651453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
654890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
654891     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)'' 
654898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
654899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
654900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
654900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
654901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
654908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
654910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
654911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
654912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
654913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
655004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
655007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
655009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
655010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
655010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
655011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
655012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
655105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
655106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
655107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
655108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
655109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
655110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
655110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
655111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
655185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
655187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
655258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
655262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
655266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
655267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
655268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
655269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
655278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
655357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
655358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
655359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
655360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
655430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
655439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
655439     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)'' 
655442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
655443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
655444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
655444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
655445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
655455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
655457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
655458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
655459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
655459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
655546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
655547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
655549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
655549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
655550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
655638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
655642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
655644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
655644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
655645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
655646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
655646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
655743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
655745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
655746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
655747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
655748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
655748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
655749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
655750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
655751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
655752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
655753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
655753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
655754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
655754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
655755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
655839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
655840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
655846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
655920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
655997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
655998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
655999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
656000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
656000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
656001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
656001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
656001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
656002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
656083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
656089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
656174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
656175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
656176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
656177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
656177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
656178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
656178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
656179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
656183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
656184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
656303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
656308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
656312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
656406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
656407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
656407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
656408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
656408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
656409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
656409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
656410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
656461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
656462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
656462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
656463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
656463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
656468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
656473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
656583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
656667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
656668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
656669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
656669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
656828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
656912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
656912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
659867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
659873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
659874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
659875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
659875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
659988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
659989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
659990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
659991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
659992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
660095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
663213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
666432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
666437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
666438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
666439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
666440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
666553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
666555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
666556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
666557     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)' ...' 
666559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
667677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
667677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
667678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
670268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
671074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
671075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
671075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
671081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
671092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
671095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
671097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
671097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
671101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
671103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
671105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
671108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
671109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
671117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
671119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
671119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
671165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
671166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
671167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
671167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
671168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
671228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
671229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
671230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
671231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
671231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
671253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
671254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
671254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
671255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
671256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
671257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
671332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
671332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
671333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
671334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
671335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
671335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
671418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
671419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
671419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
671419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
671420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
671421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
671421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
671422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
671422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
671423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
671423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
671423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
671424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
671424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
671425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
671425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
671425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
671426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
671427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
671429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
671461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
671462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
671513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
671514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
671515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
671517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
671518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
671518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
671563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
671565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
671566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
671568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
671569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
671570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
671570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
671616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
671618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
671621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
671671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
671729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
671729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.2ns 
671730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
674145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
674961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
674992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.35ms