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

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

tests
0

failures
0

ignored
10m52.47s

duration
100%

successful

Tests

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

Standard output

283        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
305        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.01ms 
515        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536        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)

1451       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1455       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1459       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1459       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2778       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8187       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.67s 
8266       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8300       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.7ns 
8315       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8317       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.79ms 
8323       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
11181      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12153      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
12168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.69ms 
12171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
14855      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms 
15730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.4ns 
15731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
18346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19164      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
19166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19166      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
19167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
21720      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
22570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 646.7ns 
22571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
25069      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25935      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.32ms 
25937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
25938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
28420      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29278      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.71ms 
29283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 636.39ns 
29285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
31775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32594      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 657.5ns 
32596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.9ns 
32598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
35078      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35900      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.6ns 
35903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35904      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.6ns 
35905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
38380      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39184      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.4ns 
39187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.55ms 
39189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
41638      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42442      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 631.7ns 
42443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.3ns 
42445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
44888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45689      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.2ns 
45692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.8ns 
45693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
48112      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49015      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.09ms 
49019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49019      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.4ns 
49021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
51463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.16ms 
52302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.7ms 
52304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
54722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55694      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.48ms 
55697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
55698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58153      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
58153      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58943      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
58944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58945      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
58945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
61389      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62163      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
62165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62166      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242ns 
62167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
64597      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65385      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65432      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.88ms 
65434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 
65436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
67864      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68667      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
68669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.1ns 
68670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71057      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
71057      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71866      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.84ms 
71869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.3ns 
71874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
74297      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75103      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
75105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
75106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77511      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
77512      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.91ms 
78339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.68ms 
78342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
80761      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81566      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
81568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
81568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
83971      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84754      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998ns 
84756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274ns 
84757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
87171      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88010      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.23ms 
88014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.2ns 
88015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90408      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
90409      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91251      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.81ms 
91254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.3ns 
91255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
93685      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.21ms 
94506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
94507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
96907      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms 
97687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97688      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 837.7ns 
97689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
100102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
100902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
100903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
103318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.99ms 
104092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
104093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
106491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
107279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
107280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
109698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
110499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
110500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
112884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
113672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
113672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
116096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
116877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
116878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
119280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
120059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
120069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
120070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
120070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
120071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
122489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
123267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
123316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.83ms 
123319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
123319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.9ns 
123334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
125751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
126529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
126545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
126547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
126547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.8ns 
126548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
128978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.35ms 
129814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns 
129815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
132198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
132997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
132998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
135394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
136190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
136192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
136192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.9ns 
136193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
138609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
139375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
139423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.45ms 
139426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
139426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
139428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
141848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
142633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
142636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
142638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
142638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 
142639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
145056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
145823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
145827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
145829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
145829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.9ns 
145830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
148269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
149093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
149101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
149102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
149102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
149103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
151642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
152417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
152420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
152421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.5ns 
152422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
154830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
155613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
155630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
155632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
155632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
155632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
158042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
158821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
158834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
158839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
158839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
158839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
161226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
162015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
162018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
162019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
162020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.1ns 
162020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
164433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
165211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
165216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
165218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
165218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 
165219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
167616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
168394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
168398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
168400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
168400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.4ns 
168401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
170811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
171591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
171658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.77ms 
171660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
171660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.1ns 
171661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
174053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
174835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
174914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.87ms 
174917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
174917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 
174918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
177315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
178093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
178096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
178098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
178099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.8ns 
178100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
180494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
181255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
181315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.46ms 
181317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
181322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.91ms 
181323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
183731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
184512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
184540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.96ms 
184542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
184542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232ns 
184543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
186952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
187724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
187727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
187732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
187732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 553.7ns 
187733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
190137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
190917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
191054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.74ms 
191057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
191057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.8ns 
191058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
193485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
194275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
194292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
194293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
194293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
194296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
196692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
197469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
197476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
197477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
197477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
197478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
199887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
200666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
200681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
200683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
200683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
200684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
203077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
203850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
203861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
203863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
203864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
203864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
206239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
207007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
207010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
207016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
207016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.5ns 
207017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
209378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
210152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
210157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
210158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
210158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
210159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
212539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
213310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
213332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.65ms 
213336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
213336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.3ns 
213338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
215707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
216482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
216498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
216499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
216499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
216499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
218871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
219646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
219662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
219663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
219664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.3ns 
219664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
222047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
222800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
222804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
222805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
222805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.1ns 
222806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
225193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
225964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
225968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
225969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
225969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
225970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
228342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
229093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
229098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
229099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
229099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
229100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
231497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
232276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
232279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
232280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
232280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
232281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
234672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
235426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
235428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.1ns 
235429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
235429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
235430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
237815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
238586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
238590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
238591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
238591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
238592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
240968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
241741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
241743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.7ns 
241745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
241745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.1ns 
241746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
244109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
244885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
244934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.12ms 
244936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
244936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203ns 
244937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
247339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
248112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
248163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.12ms 
248165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
248165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
248166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
250538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
251311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
251346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.05ms 
251347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
251347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
251348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
253730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
254502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
254549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.79ms 
254552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
254552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.6ns 
254553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
256918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
257690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
257718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.13ms 
257720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
257720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
257721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
260103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
260878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
260923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.91ms 
260925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
260925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.9ns 
260926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
263318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
264099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.1ms 
264100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
264100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
264101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
266476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
267248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
267266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.26ms 
267267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
267267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
267268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
269652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
270410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
270434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ms 
270435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
270435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
270436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
272827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
273599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
273617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.86ms 
273618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
273618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
273619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
276002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
276776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
276803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.93ms 
276805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
276805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
276805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
279170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
279943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
279967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.05ms 
279968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
279968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
279969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
282370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
283167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.5ms 
283168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
283168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
283169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
285531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
286302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
286326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.9ms 
286327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
286328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
286328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
288705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
289480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
289500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
289502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
289502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.8ns 
289503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
291866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
292637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
292660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.25ms 
292661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
292661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
292662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
295040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
295811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
295835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.73ms 
295837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
295837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
295837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
298217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
298971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
298978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
298979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
298979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
298979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
301358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
302146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
302147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
302148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
302148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
304525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
305279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
305282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
305283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
305283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
305284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
307655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
308426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
308428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.9ns 
308429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
308429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
308430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
310803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
311558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
311561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.7ns 
311562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
311562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
311562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
313941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
314726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
314740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
314744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
314744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns 
314745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
317122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
317897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
317903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
317904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
317904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
317905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
320268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
321051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
321052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
321052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
321052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
323434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
324205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
324208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
324209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
324209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
324210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
326570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
327342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
327344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.8ns 
327345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
327345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
327346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
329720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
330492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
330498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
330499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
330499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
330499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
332860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
333632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
333634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632ns 
333635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
333635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
333636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
336018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
336790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
336792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.7ns 
336794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
336794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
336794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
339171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
339924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
339926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.9ns 
339927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
339927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
339927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
342324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
343159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
343162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
343164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
343164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
343164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
345541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
346314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
346322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
346323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
346323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
346324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
348687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
349460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
349464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
349465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
349465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
349466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
351843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
352618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
352625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
352626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
352626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
352626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
355002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
355773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
355776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
355777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
355778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
355778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
358138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
358909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
358925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
358927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
358928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.7ns 
358928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
361304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
362082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
362086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
362087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
362087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
362087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
364455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
365227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
365230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
365231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
365231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
365232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
367584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
368371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
368374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
368375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
368375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
368376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
370742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
371514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
371530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.47ms 
371531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
371531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
371532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
373971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
374742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
374746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 482.7ns 
374748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
374748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
374749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
377091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
377860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
377897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.47ms 
377898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
377898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
377899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
380267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
381040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
381045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
381048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
381048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.8ns 
381049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
383418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
384190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
384211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
384212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
384212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
384213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
386589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
387362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
387382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.86ms 
387383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
387384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
387384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
389770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
390528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
390551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
390552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
390552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
390553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
392925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
393697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
393699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.3ns 
393700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
393700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
393701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
396074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
396846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
396851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
396852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
396852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
396853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
399233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
400009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
400012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
400013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
400013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
400013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
402382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
403157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
403159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.9ns 
403160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
403160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
403161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
405529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
406309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
406312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
406316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
406316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.9ns 
406317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
408682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
409458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
409461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
409462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
409462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
409463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
411834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
412610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
412612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
412614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
412614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
412614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
414984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
415764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
415779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
415780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
415780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
415781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
418153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
418931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
418943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
418946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
418946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.7ns 
418947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
421319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
422100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
422110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
422111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
422111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
422112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
424474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
425257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
425268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
425269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
425269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
425270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
427636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
428422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
428426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
428428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
428428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
428430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
430797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
431578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
431584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
431585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
431585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
431586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
433961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
434748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
434750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.2ns 
434751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
434751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
434751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
437112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
437895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
437898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
437899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
437899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
437900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
440263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
441044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
441046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.6ns 
441047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
441047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
441048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
443411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
444195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
444205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
444206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
444206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
444207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
446574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
447358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
447361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
447363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
447363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
447363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
449729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
450510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
450516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.51ms 
450517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
450517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
450518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
452886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
453668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
453670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.7ns 
453671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
453671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
453672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
456044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
456829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
456831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.5ns 
456832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
456832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
456833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
459201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
459985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
459988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
459989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
459989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
459990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
462462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
463267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
463270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
463271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
463271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
463271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
465636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
466419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
466422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
466423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
466423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
466424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
468790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
469573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
469576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
469577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
469577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
469577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
471944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
472725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
472732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
472733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
472734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.2ns 
472734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
475104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
475887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
475890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
475891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
475891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
475892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
478286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
479070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
479082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
479083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
479084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166ns 
479084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
481451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
482235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
482237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.7ns 
482238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
482238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
482239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
484604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
485386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
485393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
485394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
485394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
485395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
487759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
488541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
488544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.3ns 
488545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
488545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
488545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
490909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
491692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
491694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.6ns 
491695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
491695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
491696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
494079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
494861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
494866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
494867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
494867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
494868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
497230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
498013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
498015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
498016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
498016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
498017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
500387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
501170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
501173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
501174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
501174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
501175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
503539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
504325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
504329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
504330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
504330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
504331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
506719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
507502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
507507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
507508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
507508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
507509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
509875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
510658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
510672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
510673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
510673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
510673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
513036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
513818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
513833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms 
513834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
513834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
513835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
516215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
516997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
517006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
517007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
517008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
517008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
519372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
520156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
520167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ms 
520168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
520168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
520168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
522557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
523341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
523365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.38ms 
523366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
523367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
523367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
525741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
526524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
526549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.26ms 
526550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
526550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
526551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
528915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
529701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
529724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
529725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
529725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
529725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
532115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
532900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
532914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
532915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
532915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
532916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
535294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
536080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
536120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.44ms 
536122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
536122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
536123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
538511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
539294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
539339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.5ms 
539341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
539341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
539341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
541708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
542493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
542530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.64ms 
542531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
542532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
542532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
544925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
545710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
545751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.75ms 
545752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
545752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
545753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
548128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
548935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
548978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.21ms 
548979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
548979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
548980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
551367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
552172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
552288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.83ms 
552289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
552289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
552290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
554684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
555472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
555483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
555485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
555485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.4ns 
555486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
557861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
558646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
558653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
558654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
558654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
558654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
561037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
561822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
561827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
561828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
561828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
561829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
564196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
564997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
565014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
565015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
565015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
565016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
567380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
568163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
568173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
568174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
568175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
568175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
570558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
571345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
571348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
571349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
571349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
571350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
573758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
574604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
574621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
574623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
574623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.3ns 
574624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
577117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
577915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
577932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
577933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
577933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
577934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
580328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
581114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
581132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.86ms 
581133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
581133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
581134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
583536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
584355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
584358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
584359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
584359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
584360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
586728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
587511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
587515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
587516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
587516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
587517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
589891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
590677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
590682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
590684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
590684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
590684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
593072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
593858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
593863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
593864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
593865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
593865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
596244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
597029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
597094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.56ms 
597096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
597096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
597096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
599496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
600282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
600313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.98ms 
600315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
600315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173ns 
600316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
602676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
603478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
603499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.73ms 
603500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
603500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
603501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
605864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
606647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
606649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297.4ns 
606650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
606650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
606651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
609074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
609894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
610121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 215.02ms 
610124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
610124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
610125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
612490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
613277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
613326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.75ms 
613327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
613327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
613327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
615714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
616499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
616501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 321.3ns 
616502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
616502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
616503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
618866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
619651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
619653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.8ns 
619654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
619654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
619654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
622031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
622815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
622817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325.3ns 
622818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
622818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
622818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
625183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
625968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
625970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.8ns 
625971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
625971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
625971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
628359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
629142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
629232     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
629248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.64ms 
629250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
629251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.2ns 
629252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
631631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
632415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
632461     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
632462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.02ms 
632463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
632463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
632465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
634868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
635656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
635657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
635683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
635720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
635738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
635742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
635748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
635751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
635752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
635754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
635763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
635765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
635767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
635768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
635912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
635913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
635914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
635915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
635916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
636022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
636023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
636024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
636025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
636027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
636027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
636178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
636180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
636181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
636182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
636183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
636184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
636296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
636298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
636299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
636299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
636301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
636302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
636309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
636310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
636310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
636312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
636313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
636314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
636321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
636322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
636323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
636324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
636325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
636326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
636462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
636463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
636464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
636572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
636573     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)'' 
636576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
636577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
636578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
636579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
636579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
636580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
636584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
636586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
636587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
636587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
636588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
636687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
636692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
636694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
636694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
636695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
636696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
636698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
636807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
636809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
636809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
636811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
636811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
636812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
636812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
636813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
636900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
636901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
636985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
636988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
636992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
636993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
636994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
636995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
636995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
636995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
636996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
636997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
637004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
637007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
637092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
637093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
637094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
637095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
637096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
637096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
637096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
637097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
637177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
637183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
637290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
637293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
637295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
637296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
637297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
637298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
637428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
637432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
637434     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)'' 
637436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
637438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
637438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
637440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
637441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
637448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
637454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
637455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
637456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
637538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
637540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
637541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
637542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
637542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
637543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
637647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
637650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
637651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
637652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
637653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
637654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
637654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
637655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
637742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
637744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
637816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
637817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
637818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
637822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
637825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
637829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
637941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
637942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
637943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
637944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
637954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
638033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
641502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
641503     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)'' 
641510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
641511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
641511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
641512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
641512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
641520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
641522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
641523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
641523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
641524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
641615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
641618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
641619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
641620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
641620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
641621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
641621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
641711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
641712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
641713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
641715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
641716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
641716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
641716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
641717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
641795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
641796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
641872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
641876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
641880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
641880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
641881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
641882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
641891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
641970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
641971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
641971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
641972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
642047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
642055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
642056     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)'' 
642058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
642058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
642059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
642059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
642060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
642070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
642071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
642072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
642072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
642073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
642155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
642157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
642158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
642159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
642160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
642246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
642250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
642251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
642252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
642252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
642253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
642254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
642348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
642349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
642350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
642351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
642352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
642353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
642353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
642354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
642355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
642356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
642357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
642357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
642357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
642358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
642358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
642440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
642441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
642447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
642559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
642635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
642636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
642637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
642637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
642638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
642638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
642639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
642639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
642640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
642720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
642725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
642809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
642810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
642811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
642812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
642812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
642812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
642813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
642813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
642818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
642819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
642893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
642898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
642903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
642996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
642997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
642997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
642998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
642999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
642999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
642999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
643000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
643051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
643052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
643052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
643053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
643053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
643058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
643063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
643172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
643254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
643255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
643256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
643257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
643413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
643504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
643504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
646358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
646363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
646364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
646365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
646366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
646474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
646475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
646476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
646477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
646478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
646577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
649361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
652346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
652351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
652352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
652352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
652353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
652460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
652461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
652462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
652463     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)' ...' 
652465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
653551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
653551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
653551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
656012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
656818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
656820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
656820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
656826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
656837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
656840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
656841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
656842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
656845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
656847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
656849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
656852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
656852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
656860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
656861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
656862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
656903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
656904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
656905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
656905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
656906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
656962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
656963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
656964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
656965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
656965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
656969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
656969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
656970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
656971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
656971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
656972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
657044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
657044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
657045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
657046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
657047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
657047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
657124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
657125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
657126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
657126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
657127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
657128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
657128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
657129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
657130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
657130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
657130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
657131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
657131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
657132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
657132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
657133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
657133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
657134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
657135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
657138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
657174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
657176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
657228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
657229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
657231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
657232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
657232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
657233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
657274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
657276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
657277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
657279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
657280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
657280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
657281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
657320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
657322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
657325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
657372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
657422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
657423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.3ns 
657423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
659891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
660771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
660801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.6ms